Math Autoformalization with Gemini

Translate informal math into verified Lean 4 proofs using Gemini and a retry loop.

Introduction

30 Second Summary

Mathematical proofs underpin the security of every message you send and every transaction you make online. Translating those proofs into something a computer can verify is still a painstaking, manual process.

In this project, you will build an autoformalization pipeline that takes a plain English math statement, uses Gemini to translate it into a formal Lean 4 proof, and verifies it automatically. When proofs fail, your tool classifies the error and retries with targeted feedback.

What You'll Build

Type "For all natural numbers n, n + 0 = n" into your terminal and watch your pipeline generate a formal proof, run it through the Lean compiler, and report whether it verified.

By the end of this project, you'll have:

  • A command-line tool where you type an informal math statement and get back a verified Lean 4 proof generated by Gemini.
  • An error-feedback retry loop that catches failed proofs, classifies the compiler error, and re-prompts the LLM with targeted repair instructions until it produces a valid proof.
  • A batch test suite you can run across theorems of varying difficulty to see a scorecard of passes versus failures.
  • Secret Mission: Add multi-candidate sampling with majority voting to boost your pipeline's accuracy.

Do I need to know Lean or formal math?

No. This project teaches you the autoformalization pattern from scratch. You just need intermediate Python knowledge, such as writing scripts and using libraries.

Before We Start

Before you write any code, let's commit to the destination. You're building an autoformalization pipeline that connects an LLM (Gemini) to a proof assistant (Lean 4), using the proof assistant's error messages to teach the LLM to fix its own mistakes.

Set Up Your Toolchain

Your autoformalization pipeline needs three tools working together. Lean 4 is the proof compiler that verifies whether a mathematical proof is correct. LeanInteract is the Python bridge that lets your script talk to Lean. The Gemini SDK is the LLM that will generate proof candidates.

Without all three, no part of the pipeline can run. In this step, you will install each tool, wire up your API key, and confirm everything imports cleanly so the rest of the project builds on solid ground.

In this step, get ready to:
  • Install Lean 4 via the elan version manager.
  • Install the LeanInteract and Gemini Python packages.
  • Set up your Gemini API key and verify both libraries import successfully.
Install Lean 4 via elan

Lean 4 is the proof assistant that will verify every proof your pipeline generates. You install it through elan, the Lean version manager (similar to how nvm manages Node versions).

  • Open your terminal and install elan by running this command:

macOS

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

What does this command do?

This downloads and runs the elan installer script. The installer will ask you about editing your shell config to add Lean to your PATH. Press Enter to accept the defaults.

  • After the installer finishes, close and reopen your terminal so the new PATH takes effect.

Linux

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

What does this command do?

This downloads and runs the elan installer script. The installer will ask you about editing your shell config to add Lean to your PATH. Choose 1 to accept the default install option.

  • After the installer finishes, run the following command to add elan to your current session:
  • Alternatively, close and reopen your terminal.
source $HOME/.elan/env

Windows

Open Command Prompt or PowerShell (version 7.4.1 or later).

curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

What does this command do?

The first line downloads the elan installer script. The second line runs it with elevated permissions. The third line cleans up the script file afterwards.

  • After the installer finishes, close and reopen your terminal so the new PATH takes effect.

Windows also needs long path support enabled to prevent errors. Open an Administrator PowerShell and run these two commands:

New-ItemProperty -Path "HKLM:\SYSTEM\CurrentControlSet\Control\FileSystem" -Name LongPathsEnabled -Value 1 -PropertyType DWord -Force
git config --system core.longpaths true

Why enable long paths?

Lean and LeanInteract generate deeply nested file paths that can exceed the Windows 260-character path limit. Without this fix, builds silently fail with confusing errors.

  • Verify elan installed correctly by running:
lean --version

Before you check the output, what do you expect to see if elan installed correctly?

✔️ I see a Lean version number

Lean is ready. You should see output like Lean (version 4.x.x, ...). The exact version depends on your elan default toolchain.

ⓧ I see an older version or unexpected output

Elan may have installed a different default toolchain. This is fine for now. LeanInteract will automatically download the specific Lean version your project needs (4.18.0) when you first run a script.

ⓧ Command not found

  • Make sure you closed and reopened your terminal after running the installer.
  • On macOS/Linux, run source $HOME/.elan/env to load the path manually.
  • On Windows, open a brand new Command Prompt or PowerShell window.
  • If it still fails, re-run the install command from the platform tab above.

Still seeing command not found?

The elan installer adds Lean to your PATH by modifying your shell config file. If you use a non-default shell (like fish or zsh with a custom config), you may need to add ~/.elan/bin to your PATH manually.

Help me troubleshoot my elan installation. I ran the installer but lean --version says command not found.

Install the Python packages

LeanInteract and the Gemini SDK are both Python packages. LeanInteract requires Python 3.10 or later and elan version 4.0.0 or later.

  • Verify your elan version meets the minimum by running:
elan --version

You should see a version number of 4.0.0 or higher.

  • Install both packages by running:
pip install lean-interact google-genai

What are these packages?

lean-interact is the Python bridge to Lean 4. It manages a Lean REPL behind the scenes so your Python script can send code to Lean and get back results.

google-genai is the official Gemini API client. It lets you call gemini-2.5-flash (and other models) from Python.

Seeing install errors?

Make sure you are running Python 3.10 or later. Check with python --version (or python3 --version on macOS). If your version is older, upgrade Python before continuing.

Help me fix my pip install error for lean-interact and google-genai.

Get a Gemini API key and verify your setup

The Gemini API needs an API key to authenticate your requests. The free tier covers all the usage in this project at no cost.

  • Go to Google AI Studio in your browser.
  • Sign in with your Google account.
  • Click Get API Key.
  • Click Create API Key.
  • Copy the key. You will only see it once.

Keep your API key safe

Do not share your API key or commit it to version control. You will paste it into a terminal command next, which keeps it out of your code files.

  • Set the API key as an environment variable by running this command (paste your actual key in place of the placeholder):

macOS

export GOOGLE_API_KEY=your-api-key-here

Linux

export GOOGLE_API_KEY=your-api-key-here

Windows

set GOOGLE_API_KEY=your-api-key-here

Why an environment variable?

Storing the key in an environment variable keeps it out of your source code. Your Python script reads it with os.environ.get("GOOGLE_API_KEY") so the key never appears in autoformal.py.

Now confirm that both libraries import correctly. This is the moment of truth for your entire toolchain.

  • Verify LeanInteract by running:
python -c "from lean_interact import LeanREPLConfig; print('LeanInteract OK')"
  • Verify the Gemini SDK by running:
python -c "from google import genai; print('Gemini SDK OK')"

What do you expect to see if everything is installed correctly?

✔️ Both commands print OK

Your toolchain is fully set up. You see LeanInteract OK and Gemini SDK OK printed without errors.

ⓧ I see a ModuleNotFoundError

  • Make sure you ran pip install lean-interact google-genai in the same Python environment you are using now.
  • If you use python3 instead of python, try python3 -c instead.
  • On some systems, pip and pip3 point to different Python installations. Use pip3 install lean-interact google-genai if needed.

One of the imports failed?

If LeanInteract fails, confirm that elan is on your PATH by running elan --version. LeanInteract needs elan 4.0.0 or later. If the Gemini import fails, re-run the pip install command and check for error messages.

Help me debug why my Python import is failing for lean-interact or google-genai.

Your toolchain is locked and loaded. Next up, you will write your first Python script that sends a hardcoded Lean proof to the compiler and sees whether it passes or fails.

Send Your First Statement to Lean

Your toolchain is ready. Lean 4, LeanInteract, and the Gemini SDK are all installed and importing cleanly.

Before connecting an LLM, you need to confirm that the verification half of the pipeline actually works from Python. If you skip this and jump straight to Gemini, you won't know whether a failure is the LLM's fault or Lean's. In this step, you'll send two theorems directly to the Lean compiler and see the raw pass/fail signal your pipeline will rely on.

In this step, get ready to:
  • Create autoformal.py with functions to initialize the Lean server and verify proofs.
  • Send a correct and a broken theorem to see the difference between success and failure.
Create autoformal.py and verify a correct proof

Your pipeline needs two core abilities: starting a Lean server from Python, and sending code to that server for verification. You'll build both as reusable functions in a single file.

  • Move to your Desktop by running this command:
cd ~/Desktop
  • Create your project folder and move into it by running these commands:
mkdir autoformal-pipeline
cd autoformal-pipeline
  • Confirm the folder exists by running:
ls

You should see the autoformal-pipeline folder listed in the output.

  • Open VS Code in this folder by running:
code .
  • Create a new file called autoformal.py in the autoformal-pipeline folder.
  • Add the imports and two core functions by copying this code into autoformal.py:
import sys
import os
import re

from google import genai
from google.genai import types
from lean_interact import LeanREPLConfig, LeanServer, Command

def create_lean_server():
    """Initialize and return a LeanInteract server."""
    # Pin to Lean 4.18.0 for stable, reproducible results
    config = LeanREPLConfig(lean_version="4.18.0")
    server = LeanServer(config)
    return server

def verify_lean_code(server, code):
    """Send Lean code to the server and return (success, message)."""
    # Run the code as a Lean command
    result = server.run(Command(cmd=code))
    if result.messages:
        # Filter for error-severity messages only
        error_msgs = [m for m in result.messages if m.severity == "error"]
        if error_msgs:
            error_text = "\n".join(m.text for m in error_msgs)
            return False, error_text
    return True, "Proof verified successfully."

What does this code do?

  • create_lean_server() initializes a LeanInteract server pinned to Lean version 4.18.0. This is the bridge between Python and the Lean compiler.
  • verify_lean_code() sends a string of Lean code to that server and checks the result. If Lean returns any error-severity messages, the function returns False with the error text. Otherwise it returns True.
  • Now add a code-extraction helper and a main block that sends a correct theorem to Lean. Copy this code below verify_lean_code in autoformal.py:
def extract_lean_code(response_text):
    """Extract Lean code from an LLM response, handling code fences."""
    # Try to match ```lean or ```lean4 code fences
    match = re.search(r"```(?:lean4?|lean)\n(.*?)```", response_text, re.DOTALL)
    if match:
        return match.group(1).strip()
    # Fall back to generic code fences
    match = re.search(r"```\n(.*?)```", response_text, re.DOTALL)
    if match:
        return match.group(1).strip()
    # No fences found, return the raw text
    return response_text.strip()

if __name__ == "__main__":
    server = create_lean_server()
    # A correct theorem: simp can prove n + 0 = n
    correct = "theorem add_zero (n : Nat) : n + 0 = n := by simp"
    print("Correct theorem result:")
    print(verify_lean_code(server, correct))

What does this code do?

  • extract_lean_code() strips code fences from LLM responses. You won't use it in this step, but it will be essential when you connect Gemini in the next step.
  • The if __name__ == "__main__" block creates a Lean server and sends a correct theorem: "for all natural numbers n, n + 0 = n". The simp tactic handles this proof because n + 0 = n is true by definition in Lean's natural number arithmetic.
  • Save autoformal.py.
  • Run the script by entering this command in your terminal:
python autoformal.py

First run takes a few minutes

The first time you run the script, LeanInteract downloads and builds the Lean REPL behind the scenes. This can take a few minutes depending on your machine. Subsequent runs will be much faster.

You should see output like this:

Correct theorem result:
(True, 'Proof verified successfully.')

The tuple (True, 'Proof verified successfully.') confirms that Lean accepted the proof. The verification half of your pipeline works.

Don't see the success message?

  • If you see a timeout or download error, check your internet connection. LeanInteract needs to download the Lean REPL on the first run.
  • If you see an import error for lean_interact, make sure you installed it with pip install lean-interact in Step 1.
  • On Windows, if you see long-path errors, confirm you ran the long-path registry fix from Step 1.

Help me debug my LeanInteract server connection.

Send a broken proof to see what failure looks like

A successful proof is only half the picture. Your pipeline needs to detect failures too. You'll send a theorem that uses the wrong tactic so you can see what a Lean error looks like from Python.

  • In autoformal.py, find the if __name__ == "__main__": block at the bottom of the file.
  • Find this code:
if __name__ == "__main__":
    server = create_lean_server()
    # A correct theorem: simp can prove n + 0 = n
    correct = "theorem add_zero (n : Nat) : n + 0 = n := by simp"
    print("Correct theorem result:")
    print(verify_lean_code(server, correct))
  • Replace the entire if __name__ == "__main__": block with this updated version that adds a broken theorem:
if __name__ == "__main__":
    server = create_lean_server()
    # A correct theorem: simp can prove n + 0 = n
    correct = "theorem add_zero (n : Nat) : n + 0 = n := by simp"
    # A broken theorem: ring fails on natural numbers
    broken = "theorem bad (n : Nat) : n + 0 = n := by ring"
    print("Correct theorem result:")
    print(verify_lean_code(server, correct))
    print("\nBroken theorem result:")
    print(verify_lean_code(server, broken))

Why does the ring tactic fail here?

The ring tactic is designed to prove equalities in commutative rings. Natural numbers are not a ring because they lack negation. The simp tactic works because n + 0 = n is true by definition in Lean's natural number arithmetic.

This is exactly the kind of subtle tactic mismatch that LLMs frequently produce. Your pipeline needs to catch these errors and feed them back to the LLM for repair.

  • Save autoformal.py.

Before you run this, what do you expect to see for each theorem? Think about which one should pass and which should fail.

  • Run the script again:
python autoformal.py

You should see one success and one failure. The correct theorem returns True, and the broken theorem returns False with an error message from Lean about the ring tactic failing.

This is the raw signal your entire pipeline will use. A successful proof returns (True, 'Proof verified successfully.'). A failed proof returns (False, '<error details>').

Both theorems showing errors?

  • Double-check that the correct theorem string uses simp, not ring. A typo here would cause both to fail.
  • Make sure you saved autoformal.py before running it again.

Help me debug why both my Lean theorems are failing.

✔️ Awesome, I've got everything!

Great. Double check you've saved autoformal.py and you can see one passing and one failing theorem in your terminal.

ⓧ I'd like to double check the full code

Your autoformal.py should contain these sections in order. Scroll up and confirm each is present:

  • Imports: sys, os, re, genai, types, LeanREPLConfig, LeanServer, Command.
  • create_lean_server() function that creates a LeanREPLConfig with lean_version="4.18.0" and returns a LeanServer.
  • verify_lean_code(server, code) function that runs a Command, filters for error messages, and returns a (success, message) tuple.
  • extract_lean_code(response_text) function that uses regex to strip code fences from LLM responses.
  • An if __name__ == "__main__": block that sends both correct (using simp) and broken (using ring) theorems and prints both results.

You've proven that the verification half of your pipeline works. Lean gives you a clean pass/fail signal for any code you send it. Next up, you'll connect Gemini to generate the Lean code automatically from plain English math statements.

Generate Proofs with Gemini

In the last step you proved that LeanInteract can talk to Lean 4 from Python. You saw a correct proof pass and a broken proof fail. Now you need the other half of the pipeline: an LLM that can translate plain English math into formal Lean 4 code.

In this step, you will write a function that prompts Gemini to generate Lean proofs, then wire it to your existing verification. LLMs are unreliable at formal syntax, so some proofs will fail. That failure is exactly the signal your retry loop will use in the next step.

In this step, get ready to:
  • Write a function that prompts Gemini to generate Lean 4 proofs from informal math.
  • Connect proof generation to Lean verification via the command line.
  • Test with easy and hard statements to see where the pipeline breaks.
Write the proof generation function

Your pipeline needs a function that takes an informal math statement (like "For all natural numbers n, n + 0 = n"), wraps it in a carefully crafted prompt, sends it to Gemini, and extracts just the Lean 4 code from the response.

  • In autoformal.py, find the extract_lean_code function.
  • Add the following generate_proof function directly below it:
def generate_proof(client, statement):
    """Ask Gemini to formalize an informal math statement into Lean 4."""
    prompt = f"""You are a formal mathematics assistant. Translate the following informal
math statement into a valid Lean 4 theorem with a complete proof.

Rules:
- Output ONLY the Lean 4 code inside a single code fence.
- Use a `theorem` declaration with a `by` tactic proof.
- Do NOT import anything. Only use tactics available in Lean 4 core (simp, omega, ring, exact, intro, apply, rfl, trivial, decide, cases, induction, rw).
- The theorem name should be `auto_theorem`.
- Make sure the proof is complete (no `sorry`).

Informal statement: {statement}
"""
    response = client.models.generate_content(
        model="gemini-2.5-flash",
        contents=prompt,
    )
    return extract_lean_code(response.text)

What does this code do?

The prompt gives Gemini strict rules: output only Lean 4 code, use a theorem declaration with a by tactic proof, stick to core tactics, and never use sorry (a placeholder that skips the proof). These constraints steer the LLM toward code that Lean can actually compile.

The function calls client.models.generate_content with gemini-2.5-flash, then passes the raw response through extract_lean_code to strip out markdown fences and return clean Lean source.

  • Save autoformal.py.
Connect Gemini to Lean via the command line

Right now the if __name__ block at the bottom of your file still runs the hardcoded test theorems from Step 2. You need to replace it with code that reads a statement from the command line, sends it to Gemini, and verifies the result with Lean.

  • In autoformal.py, scroll to the if __name__ == "__main__": block at the bottom of the file.
  • Delete everything from that line to the end of the file.
  • Paste this new main block in its place:
if __name__ == "__main__":
    # Load the API key from the environment
    api_key = os.environ.get("GOOGLE_API_KEY")
    if not api_key:
        print("Error: Set the GOOGLE_API_KEY environment variable.")
        sys.exit(1)

    # Create the Gemini client and the Lean server
    client = genai.Client(api_key=api_key)
    server = create_lean_server()

    # Read a statement from the command line, generate a proof, and verify it
    if len(sys.argv) > 1:
        statement = " ".join(sys.argv[1:])
        lean_code = generate_proof(client, statement)
        print(f"Generated Lean code:\n{lean_code}\n")
        success, message = verify_lean_code(server, lean_code)
        print(f"Result: {'PASSED' if success else 'FAILED'}: {message}")
    else:
        print("Usage: python autoformal.py \"Your math statement here\"")

What does this code do?

This block wires both halves of your pipeline together. It loads your GOOGLE_API_KEY, creates a Gemini client, and starts a Lean server.

When you pass a statement from the command line, it calls generate_proof to get Lean code from Gemini, then calls verify_lean_code to check whether Lean accepts it. The result prints as PASSED or FAILED with the error message.

  • Save autoformal.py.

Before you run this, what do you think will happen when you ask Gemini to formalize a simple arithmetic fact like "n + 0 = n"?

  • Test the pipeline with a simple statement by running:
python autoformal.py "For all natural numbers n, n + 0 = n"

Your terminal shows the Lean code that Gemini generated, followed by the verification result. For a simple arithmetic fact like this, Gemini typically produces a correct proof using simp or omega, and Lean accepts it with PASSED.

Seeing an error about your API key?

Make sure your GOOGLE_API_KEY environment variable is still set in your current terminal session. If you opened a new terminal since Step 1, run the set command again to re-export it.

help me debug my Gemini API key error in my autoformalization script

✔️ Awesome, I've got everything!

Great. Double check you have saved autoformal.py and that Lean returned PASSED for the simple statement.

ⓧ I'd like to double check the full code

Your autoformal.py should contain these sections in order. Scroll up and confirm each one is present:

  • Imports (sys, os, re, genai, types, LeanREPLConfig, LeanServer, Command).
  • The create_lean_server() function.
  • The verify_lean_code(server, code) function.
  • The extract_lean_code(response_text) function.
  • The new generate_proof(client, statement) function you just added.
  • The new if __name__ == "__main__": block that creates a client, reads from sys.argv, and prints the result.
Test with a harder statement

Simple arithmetic plays to Lean's strengths. Real autoformalization needs to handle harder statements too. What happens when you ask Gemini to prove something that requires deeper mathematical reasoning?

Before you run this, do you think Gemini can produce a valid Lean proof that the square root of 2 is irrational?

  • Test with a harder statement by running:
python autoformal.py "The square root of 2 is irrational"

This time the result reads FAILED. Lean prints an error message showing exactly where the generated proof broke down.

Why does the harder statement fail?

Proving irrationality requires multi-step reasoning and specific lemmas that live in Lean's Mathlib library. Your prompt restricts Gemini to core tactics only, so the model has no access to those lemmas.

Even without that restriction, LLMs frequently produce syntactically plausible but logically incorrect proofs. The error messages from Lean are precise enough to diagnose exactly what went wrong. This is the gap your retry loop will close in the next step.

Your pipeline can now generate and verify proofs end to end. The problem is that a single attempt succeeds only on easy statements. Next up, you will build an error-feedback retry loop that reads Lean's error messages and coaches Gemini to fix its own mistakes.

Build the Error-Feedback Retry Loop

In the last step, you connected Gemini and Lean into a working pipeline. You can pass any informal math statement from the command line, see the generated Lean 4 code, and find out whether it passes verification.

Here's the problem: a single LLM attempt succeeds only about 35-40% of the time on formal math. When a proof fails, Lean's error messages contain precise diagnostic information about what went wrong. The core innovation in autoformalization research is feeding those error messages back to the LLM with targeted repair hints, dramatically improving success rates. In this step, you'll build that error-feedback retry loop.

In this step, get ready to:
  • Classify Lean error messages into categories like type mismatches and tactic failures.
  • Build targeted repair prompts that give Gemini specific hints for each error type.
  • Wire up a retry loop that re-prompts Gemini until the proof passes or you run out of attempts.
Write the error classifier

Lean produces different types of errors depending on what went wrong. A type mismatch is a completely different problem from an unknown identifier. By classifying each error, you can give Gemini a targeted hint instead of a generic "try again" message.

  • In autoformal.py, add the following function below generate_proof:
def classify_error(error_text):
    """Classify a Lean error message into a category."""
    error_lower = error_text.lower()
    if "type mismatch" in error_lower:
        return "type_mismatch"
    if "tactic" in error_lower and "failed" in error_lower:
        return "tactic_failed"
    if "unknown identifier" in error_lower or "unknown constant" in error_lower:
        return "unknown_identifier"
    if "expected" in error_lower and ("token" in error_lower or "command" in error_lower):
        return "syntax_error"
    return "other"

What does this code do?

The function lowercases the error text and checks for known phrases that Lean uses in its diagnostics.

  • "type mismatch" means the proof produced the wrong type for the goal.
  • "tactic" + "failed" means a tactic like simp or ring could not close the goal.
  • "unknown identifier" or "unknown constant" means the code referenced something Lean doesn't recognise (often a Mathlib lemma).
  • Anything that doesn't match falls through to "other".
  • Save autoformal.py.
  • Verify the classifier works by running this command:
python -c "from autoformal import classify_error; print(classify_error('tactic simp failed')); print(classify_error('unknown identifier foo'))"

You should see tactic_failed on the first line and unknown_identifier on the second.

Seeing a ModuleNotFoundError?

Make sure you are running the command from the same directory where autoformal.py lives. If Python can't find the file, cd into that folder and try again.

If you see a SyntaxError, double-check your quotes and parentheses in the new function. Help me fix a SyntaxError in my classify_error function in autoformal.py

Also check that classify_error is defined at the top level of the file (no extra indentation), not accidentally nested inside another function.

Build targeted repair prompts

Now that you can classify errors, you need a function that turns each category into a specific repair hint. A tactic_failed error gets advice about trying different tactics, while an unknown_identifier error warns the LLM to avoid Mathlib-specific names.

  • Below classify_error, start adding the generate_repair_prompt function with its hint dictionary:
def generate_repair_prompt(statement, failed_code, error_category, error_text):
    """Build a targeted repair prompt based on the error category."""
    category_hints = {
        "type_mismatch": "The types in your proof do not match. Check that your expressions have the correct types and consider using type annotations or coercions.",
        "tactic_failed": "The tactic you used did not close the goal. Try a different approach such as simp, omega, or exact. Consider breaking the proof into smaller steps with `have` or using `induction`.",
        "unknown_identifier": "You referenced a name that does not exist in Lean 4 core. Do NOT use any Mathlib-specific lemmas or tactics. Stick to: simp, omega, ring, exact, intro, apply, rfl, trivial, decide, cases, induction, rw.",
        "syntax_error": "There is a syntax error in your Lean code. Make sure you use correct Lean 4 syntax with proper indentation, colons, and brackets.",
        "other": "The proof failed. Read the error message carefully and try a completely different proof strategy.",
    }

    hint = category_hints.get(error_category, category_hints["other"])

What does this dictionary do?

Each key in category_hints maps to a specific, actionable instruction for Gemini. Instead of a vague "try again," the LLM receives precise guidance tuned to the failure mode.

The hint variable looks up the matching hint, falling back to the "other" hint if the category is unrecognised.

  • Still inside the same function, add the return statement directly below the hint = ... line:

    return f"""You are a formal mathematics assistant. Your previous attempt to formalize
a math statement into Lean 4 failed. Fix the proof.

Informal statement: {statement}

Your previous attempt:
```lean
{failed_code}
```

Error category: {error_category}
Error message: {error_text}

Hint: {hint}

Rules:
- Output ONLY the corrected Lean 4 code inside a single code fence.
- Use a `theorem` declaration with a `by` tactic proof.
- Do NOT import anything. Only use tactics available in Lean 4 core.
- The theorem name should be `auto_theorem`.
- Make sure the proof is complete (no `sorry`).
"""

What does this repair prompt do?

This f-string builds a second prompt for Gemini that includes everything the LLM needs to fix its mistake: the original informal statement, the failed Lean code, the error category, the raw error message, and the targeted hint.

By embedding the previous attempt and Lean's exact error text, the LLM can see precisely where its code broke and apply the category-specific advice to produce a corrected proof.

  • Save autoformal.py.
  • Verify the repair prompt function loads correctly by running:
python -c "from autoformal import generate_repair_prompt; print(type(generate_repair_prompt('test', 'sorry', 'tactic_failed', 'tactic failed')))"

You should see <class 'str'>. This confirms the function returns a string without errors.

Seeing an IndentationError?

The return statement must be indented at the same level as the hint = ... line above it (one level inside the function). Make sure there are no stray tabs mixed with spaces.

Also verify there is no code between hint = ... and return f"""... other than a single blank line. Help me fix my generate_repair_prompt function

Wire up the retry loop

You now have the two helper functions. The final piece is a run_pipeline function that ties everything together: generate an initial proof, verify it, and on failure classify the error, build a repair prompt, and ask Gemini again.

  • Below generate_repair_prompt, start adding the run_pipeline function with the initial generation and success path:
def run_pipeline(client, server, statement, max_attempts=4, verbose=True):
    """Run the full autoformalization pipeline with retry loop."""
    if verbose:
        print(f"\n{'='*60}")
        print(f"Statement: {statement}")
        print(f"{'='*60}")

    lean_code = generate_proof(client, statement)

    for attempt in range(1, max_attempts + 1):
        if verbose:
            print(f"\n--- Attempt {attempt}/{max_attempts} ---")
            print(f"Lean code:\n{lean_code}\n")

        success, message = verify_lean_code(server, lean_code)

        if success:
            if verbose:
                print(f"PASSED: {message}")
            return True, attempt, lean_code

What does this first half do?

The function prints a header showing the statement, then calls generate_proof to get the initial Lean code from Gemini.

It enters a loop of up to max_attempts (default 4). Each iteration prints the attempt number and the current candidate code, sends it to Lean via verify_lean_code, and returns immediately if the proof passes.

  • Continue adding to the same function, directly below the return True, attempt, lean_code line, still inside the for loop:

        if verbose:
            error_category = classify_error(message)
            print(f"FAILED ({error_category}): {message[:200]}")

        if attempt < max_attempts:
            error_category = classify_error(message)
            repair_prompt = generate_repair_prompt(
                statement, lean_code, error_category, message
            )
            response = client.models.generate_content(
                model="gemini-2.5-flash",
                contents=repair_prompt,
            )
            lean_code = extract_lean_code(response.text)

    return False, max_attempts, lean_code

What does the retry logic do?

When a proof fails, this code classifies the error and prints the category with the first 200 characters of the error message.

If attempts remain, it builds a targeted repair prompt using the error category and calls Gemini again with client.models.generate_content. The new candidate replaces lean_code, and the loop runs another verification cycle. After all attempts are exhausted, the function returns failure.

  • Save autoformal.py.
  • Verify the new function loads without syntax errors by running:
python -c "from autoformal import run_pipeline; print('run_pipeline loaded OK')"

You should see run_pipeline loaded OK printed to the terminal.

Seeing a SyntaxError or IndentationError?

The retry logic block must be indented inside the for loop (two levels inside the function). The final return False, max_attempts, lean_code line sits at the function level (one indent), outside the for loop.

If you see unexpected indent, check that you haven't mixed tabs and spaces. Help me fix indentation in run_pipeline

Now you need to update the script's entry point to use run_pipeline instead of calling generate_proof and verify_lean_code directly.

  • In autoformal.py, scroll to the bottom and find the if __name__ == "__main__": block.
  • Find this code:
if __name__ == "__main__":
    api_key = os.environ.get("GOOGLE_API_KEY")
    if not api_key:
        print("Error: Set the GOOGLE_API_KEY environment variable.")
        sys.exit(1)

    client = genai.Client(api_key=api_key)
    server = create_lean_server()

    if len(sys.argv) > 1:
        statement = " ".join(sys.argv[1:])
        lean_code = generate_proof(client, statement)
        print(f"Generated Lean code:\n{lean_code}\n")
        success, message = verify_lean_code(server, lean_code)
        print(f"Result: {'PASSED' if success else 'FAILED'}: {message}")
    else:
        print("Usage: python autoformal.py \"Your math statement here\"")
  • Delete everything from if __name__ to the end of the file.
  • Replace it with this new main function and entry point:
def main():
    api_key = os.environ.get("GOOGLE_API_KEY")
    if not api_key:
        print("Error: Set the GOOGLE_API_KEY environment variable.")
        print("  set GOOGLE_API_KEY=your-api-key-here")
        sys.exit(1)

    client = genai.Client(api_key=api_key)
    server = create_lean_server()

    if len(sys.argv) > 1:
        statement = " ".join(
            arg for arg in sys.argv[1:] if not arg.startswith("--")
        )
        if statement:
            run_pipeline(client, server, statement)
        else:
            print("Usage: python autoformal.py \"Your math statement here\"")
    else:
        print("Usage: python autoformal.py \"Your math statement here\"")


if __name__ == "__main__":
    main()

What changed in the entry point?

  • The logic is now wrapped in a main() function for cleaner structure.
  • The argument parser filters out flags starting with -- so you can add flags like --batch later without breaking the statement input.
  • Instead of calling generate_proof and verify_lean_code separately, the code now calls run_pipeline, which handles generation, verification, and retries in one loop.
  • Save autoformal.py.

Before you run this, think about what you expect to see. The statement "For all natural numbers n, 0 + n = n" is slightly harder than "n + 0 = n" because 0 + n requires Lean to reason about addition's definition on the left side. Do you think the first attempt will succeed, or will the pipeline need a retry?

  • Run the pipeline with this command:
python autoformal.py "For all natural numbers n, 0 + n = n"

Your terminal shows each attempt: the generated Lean code, whether it passed or failed, the error category if it failed, and the retried candidate. You should see at least one full retry cycle complete before the proof either passes or exhausts all 4 attempts.

Why does 0 + n need a retry?

In Lean 4, natural number addition is defined by recursion on the second argument. That means n + 0 = n is true by definition (rfl), but 0 + n = n requires induction. LLMs often try rfl or simp first and fail, which is exactly the kind of mistake the retry loop was designed to catch and repair.

Pipeline not retrying on failure?

If the script prints a single attempt and stops (even on failure), check that run_pipeline has the if attempt < max_attempts: block that builds a repair prompt and calls Gemini again. The retry logic must be inside the for loop.

If you see Error: Set the GOOGLE_API_KEY environment variable, re-set your API key by running:

set GOOGLE_API_KEY=your-api-key-here

Then try the command again. Help me debug my autoformalization retry loop

✔️ Awesome, I've got everything!

Great. Double check you've saved autoformal.py and move on.

ⓧ I'd like to double check the full code

Your autoformal.py file should contain these functions in this order. Scroll through your file and confirm each one is present:

  • create_lean_server
  • verify_lean_code
  • extract_lean_code
  • generate_proof
  • classify_error (added in this step).
  • generate_repair_prompt (added in this step).
  • run_pipeline (added in this step).
  • main (added in this step).

The file ends with if __name__ == "__main__": main() as a two-line block at the very bottom.

Your pipeline can now learn from its own mistakes. Next up, you'll run a batch of test theorems to see how the retry loop performs across statements of varying difficulty and get a real accuracy scorecard.

Run a Test Suite and See the Scorecard

Your pipeline can now take a single informal math statement, translate it into Lean 4 code, verify the proof, and retry with targeted error feedback. That is a complete autoformalization loop.

A pipeline that works on one example might be a fluke, though. Running a batch of theorems with varying difficulty reveals the pipeline's real accuracy. It also shows you exactly where autoformalization breaks down: trivial arithmetic versus multi-step reasoning. In this step, you will build a test suite and a scorecard to see these patterns firsthand.

In this step, get ready to:
  • Create a list of test theorems ranging from trivial to hard.
  • Build a batch runner that prints a formatted scorecard.
  • Run the full test suite and analyze the accuracy results.
Add the test theorems

A good test suite needs theorems at different difficulty levels. Trivial statements like "n = n" test the baseline. Moderate ones like commutativity of addition push the LLM harder. Hard ones that need specific lemma imports are expected to fail, which is just as informative.

  • In autoformal.py, find the run_pipeline function. Add the following list directly below it, before the main() function:
# Test theorems of increasing difficulty
TEST_THEOREMS = [
    "For all natural numbers n, n = n",
    "For all natural numbers n, n + 0 = n",
    "For all natural numbers n, 0 + n = n",
    "For all natural numbers a and b, a + b = b + a",
    "For all natural numbers n, n * 1 = n",
    "For all natural numbers n, n * 0 = 0",
    "For all natural numbers a b c, a + (b + c) = (a + b) + c",
    "For all natural numbers a and b, a + b = b + a implies b + a = a + b",
    "If a natural number n equals 0, then n + n equals 0",
    "For all propositions P, P implies P",
]

Why these 10 theorems?

The list is ordered by difficulty. The first few (reflexivity, identity) are almost trivially provable with Lean's built-in simp and omega tactics.

The later ones (associativity, implications, propositional logic) require more sophisticated proof strategies. Statements that need Mathlib-specific lemmas will likely fail because our prompt restricts the LLM to core Lean 4 tactics only.

  • Save autoformal.py.
  • Confirm the list loads by running this command:
python -c "from autoformal import TEST_THEOREMS; print(len(TEST_THEOREMS), 'theorems loaded')"
  • You should see 10 theorems loaded in your terminal.

Seeing an import error?

Make sure you added the TEST_THEOREMS list at the module level (outside any function), between run_pipeline and main(). Check for any unclosed brackets or missing commas between the string items.

Help me debug my TEST_THEOREMS import error.

Build the batch runner and wire it up

The batch runner needs to iterate through every test theorem, run the full pipeline (generate, verify, retry), and collect the results into a formatted scorecard. This is the same evaluation approach used in research benchmarks.

  • In autoformal.py, add the following function directly below the TEST_THEOREMS list, before main():
def run_batch(client, server):
    """Run the pipeline on all test theorems and print a scorecard."""
    results = []

    # Run every theorem through the full pipeline
    for statement in TEST_THEOREMS:
        success, attempts, code = run_pipeline(
            client, server, statement, verbose=True
        )
        results.append((statement, success, attempts, code))

    # Print the scorecard header
    print(f"\n{'='*60}")
    print("SCORECARD")
    print(f"{'='*60}")
    print(f"{'Statement':<55} {'Result':<8} {'Attempts'}")
    print("-" * 75)

    # Print each result row
    passed = 0
    for statement, success, attempts, code in results:
        status = "PASS" if success else "FAIL"
        if success:
            passed += 1
        short = statement[:52] + "..." if len(statement) > 55 else statement
        print(f"{short:<55} {status:<8} {attempts}")

    # Print the final accuracy line
    print("-" * 75)
    print(f"Accuracy: {passed}/{len(results)} ({100*passed/len(results):.0f}%)")

What does this function do?

The function loops through every statement in TEST_THEOREMS, calls run_pipeline for each one, and collects the results. Each result is a tuple of the statement, whether it passed, how many attempts it took, and the final code.

After all theorems are tested, it prints a formatted table. Long statements are truncated to 52 characters so columns stay aligned. The final line shows overall accuracy as a fraction and percentage.

Now you need to update main() so the learner can trigger batch mode from the command line with a --batch flag.

  • Scroll down to the main() function.
  • Find this line:
    if len(sys.argv) > 1:
  • Replace the entire main() function with the following updated version:
def main():
    api_key = os.environ.get("GOOGLE_API_KEY")
    if not api_key:
        print("Error: Set the GOOGLE_API_KEY environment variable.")
        print("  set GOOGLE_API_KEY=your-api-key-here")
        sys.exit(1)

    client = genai.Client(api_key=api_key)
    server = create_lean_server()

    # Check for batch mode first
    if "--batch" in sys.argv:
        run_batch(client, server)
    elif len(sys.argv) > 1:
        statement = " ".join(
            arg for arg in sys.argv[1:] if not arg.startswith("--")
        )
        if statement:
            run_pipeline(client, server, statement)
        else:
            print("Usage: python autoformal.py \"Your math statement here\"")
            print("       python autoformal.py --batch")
    else:
        print("Usage: python autoformal.py \"Your math statement here\"")
        print("       python autoformal.py --batch")

What changed in main()?

The new if "--batch" in sys.argv check comes first. If the user passes --batch, it calls run_batch instead of processing a single statement. The original single-statement mode moves into an elif branch, and the usage messages now mention --batch as an option.

  • Save autoformal.py.

Before you run the batch, think about what you expect. Will all 10 theorems pass? Will the simple arithmetic ones succeed more often than the harder ones? How many do you think the pipeline will get right out of 10?

  • Run the full test suite by running this command:
python autoformal.py --batch

This will take several minutes. For each theorem, you will see Gemini's candidate proof, Lean's verdict, and any retry attempts. At the end, the scorecard table prints with a PASS or FAIL for every theorem and a final accuracy line.

What pattern should I see in the results?

Statements close to Lean's built-in tactics (basic arithmetic like "n + 0 = n", reflexivity) tend to pass easily. Commutativity and associativity of addition usually succeed because omega and simp handle them well.

Statements requiring multi-step reasoning or specific Mathlib lemmas tend to fail. Your pipeline restricts the LLM to core Lean 4 tactics, so anything beyond that is out of reach. This is the frontier of autoformalization research.

Batch run hanging or erroring out?

If the run seems stuck on the first theorem, the Lean REPL may still be building its cache. Give it a few minutes. Subsequent theorems will be much faster.

If you see a Gemini API rate limit error, wait 60 seconds and run the command again. The free tier has per-minute request limits.

Help me debug my batch run errors.

✔️ Awesome, I've got everything!

Great. Double check you have saved autoformal.py and your scorecard printed at the end of the batch run.

ⓧ I'd like to double check the full code

Your autoformal.py file is now over 30 lines, so let's verify by section. Scroll through the file and confirm you have all of these in order:

  • Imports at the top: sys, os, re, genai, types, LeanREPLConfig, LeanServer, Command.
  • create_lean_server() function.
  • verify_lean_code(server, code) function.
  • extract_lean_code(response_text) function.
  • generate_proof(client, statement) function.
  • classify_error(error_text) function.
  • generate_repair_prompt(...) function.
  • run_pipeline(client, server, statement, ...) function.
  • TEST_THEOREMS list with 10 string items (added in this step).
  • run_batch(client, server) function (added in this step).
  • main() function with --batch flag handling (updated in this step).
  • if __name__ == "__main__": block at the bottom.

Secret mission

Add Multi-Candidate Sampling with Majority Voting

Your pipeline generates one proof candidate per attempt. Research shows that generating multiple candidates at higher temperature and picking the most common one that passes type-checking can boost accuracy by 10-18 percentage points. Ready to implement this self-consistency technique and watch your scorecard improve?

Clean Up Your Resources

Clean Up Your Resources

This project runs entirely on local tools and the Gemini free tier, so there are no ongoing costs. Decide whether to keep your resources available, pause them, or delete them entirely.

Resources you used:

  • Gemini API key (free tier, no charges incurred).
  • Lean 4 installation via elan (local, no ongoing cost).
  • LeanInteract and google-genai Python packages.
  • LeanInteract REPL cache (local disk space).
  • The autoformal.py project file on your Desktop.

Keep everything running

No action needed. Choose this if you plan to keep experimenting with the autoformalization pipeline.

  • The Gemini free tier has generous limits, so your API key will not incur charges.
  • The Lean installation and LeanInteract cache use only local disk space.
  • Your autoformal.py file stays on your Desktop, ready to run.

Pause - I'll come back to this later

Nothing to pause. All resources are local or free-tier, so leaving them idle costs nothing.

  • You can free disk space by clearing the LeanInteract REPL cache. Run this command:
  • Your autoformal.py file and Lean installation will still be ready when you come back.
clear-lean-cache

Delete - I don't want to use this again

Remove all project resources and start fresh. Follow each step below.

  • Clear the LeanInteract REPL cache by running:
clear-lean-cache
  • Uninstall the Python packages by running:
pip uninstall lean-interact google-genai
  • Uninstall Lean 4 and elan by running:
elan self uninstall
  • Delete your project file. On macOS or Linux:
rm ~/Desktop/autoformal.py

On Windows:

del $HOME\Desktop\autoformal.py
  • Delete your Gemini API key if you no longer need it. Open the Google Cloud API Credentials page, find your key, click the Actions icon, select Delete API key, and confirm in the modal.
  • Unset the environment variable from your current terminal session. On macOS or Linux:
unset GOOGLE_API_KEY

On Windows (Command Prompt):

set GOOGLE_API_KEY=

Nice Work!

Nice Work!

You just built a working autoformalization pipeline that translates plain English math into verified Lean 4 proofs using Gemini. You can now type an informal statement into your terminal and watch the machine generate, verify, and iterate on a formal proof in real time.

You've learned how to:

  • Build a Python pipeline that sends informal math to Gemini, extracts the generated Lean 4 code, and verifies it through the Lean compiler using LeanInteract.
  • Implement an error-feedback retry loop that classifies Lean compiler errors into targeted categories and re-prompts the LLM with specific repair instructions to fix broken proofs.
  • Run a test suite of theorems at varying difficulty and read a scorecard that reveals where LLM-based formalization succeeds and where it breaks down.
  • Secret Mission: Completed an optional challenge to push your autoformalization pipeline further.

Ready to quiz yourself?