diff --git a/pygments/lexers/lean.py b/pygments/lexers/lean.py
index 5f1d77aec6..968043c9ca 100644
--- a/pygments/lexers/lean.py
+++ b/pygments/lexers/lean.py
@@ -7,6 +7,7 @@
     :copyright: Copyright 2006-2023 by the Pygments team, see AUTHORS.
     :license: BSD, see LICENSE for details.
 """
+import re
 
 from pygments.lexer import RegexLexer, words, include
 from pygments.token import Comment, Operator, Keyword, Name, String, \
@@ -122,6 +123,10 @@ class Lean3Lexer(RegexLexer):
         ],
     }
 
+    def analyse_text(text):
+        if re.search(r'^import [a-z]', text, re.MULTILINE):
+            return 0.1
+
 
 LeanLexer = Lean3Lexer
 
@@ -222,3 +227,7 @@ class Lean4Lexer(RegexLexer):
             ('"', String.Double, '#pop'),
         ],
     }
+
+    def analyse_text(text):
+        if re.search(r'^import [A-Z]', text, re.MULTILINE):
+            return 0.1
diff --git a/tests/test_theorem.py b/tests/test_theorem.py
new file mode 100644
index 0000000000..6e8c2a629c
--- /dev/null
+++ b/tests/test_theorem.py
@@ -0,0 +1,24 @@
+import textwrap
+import pytest
+
+from pygments.lexers.lean import Lean3Lexer, Lean4Lexer
+
+def test_lean3_import():
+    s = textwrap.dedent("""\
+        -- this is Lean 3
+        import data.nat.basic
+
+        def foo : nat := 1
+        """)
+    assert Lean3Lexer.analyse_text(s) > 0
+    assert Lean4Lexer.analyse_text(s) == 0
+
+def test_lean4_import():
+    s = textwrap.dedent("""\
+        -- this is Lean 4
+        import Mathlib.Data.Nat.Basic
+
+        def foo : Nat := 1
+        """)
+    assert Lean3Lexer.analyse_text(s) == 0
+    assert Lean4Lexer.analyse_text(s) > 0