diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
index 5127ec8b878..16a1934233c 100644
--- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
+++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
@@ -21,6 +21,17 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization {
   public class DiagnosticsTest : ClientBasedLanguageServerTest {
     private readonly string testFilesDirectory = Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles");
 
+    [Fact]
+    public async Task LeastLemmaIsVerified() {
+      var source = @"
+least lemma Foo()
+  ensures false
+{}";
+      var document = await CreateOpenAndWaitForResolve(source);
+      var diagnostics = await GetLastDiagnostics(document);
+      Assert.NotEmpty(diagnostics);
+    }
+
     [Fact(Skip = "Not implemented. Requires separating diagnostics from different sources")]
     public async Task FixedParseErrorUpdatesBeforeResolution() {
       var source = @"
diff --git a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
index d94e6012703..3f10abf1a17 100644
--- a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
@@ -160,10 +160,6 @@ public async Task<bool> VerifySymbol(FilePosition verifiableLocation, bool onlyP
     cancellationSource.Token.ThrowIfCancellationRequested();
 
     var compilation = await ResolvedCompilation;
-    var verifiable = compilation.Program.FindNode<ICanVerify>(verifiableLocation.Uri, verifiableLocation.Position.ToDafnyPosition());
-    if (verifiable == null) {
-      return false;
-    }
 
     if (compilation.ResolutionDiagnostics.Values.SelectMany(x => x).Any(d =>
           d.Level == ErrorLevel.Error &&
@@ -172,6 +168,21 @@ public async Task<bool> VerifySymbol(FilePosition verifiableLocation, bool onlyP
       throw new TaskCanceledException();
     }
 
+    var verifiable = compilation.Program.FindNode(verifiableLocation.Uri, verifiableLocation.Position.ToDafnyPosition(),
+      node => {
+        if (node is not ICanVerify) {
+          return false;
+        }
+        // Sometimes traversing the AST can return different versions of a single source AST node,
+        // for example in the case of a LeastLemma, which is later also represented as a PrefixLemma.
+        // This check ensures that we consistently use the same version of an AST node. 
+        return compilation.Verifiables!.Contains(node);
+      }) as ICanVerify;
+
+    if (verifiable == null) {
+      return false;
+    }
+
     var containingModule = verifiable.ContainingModule;
     if (!containingModule.ShouldVerify(compilation.Program.Compilation)) {
       return false;
diff --git a/docs/dev/news/4607.fix b/docs/dev/news/4607.fix
new file mode 100644
index 00000000000..6975ac819b3
--- /dev/null
+++ b/docs/dev/news/4607.fix
@@ -0,0 +1 @@
+Fix a bug that prevented certain types of lemma to be verified in the IDE 
\ No newline at end of file