I just completed the formal verification of my bachelor thesis about real time cellular automata with Lean 4, with heavy use of AI.
Over the past year, I went from fully manual mode (occasionally asking chat gpt some Lean questions) to fully automatic mode, where I barely do Lean proofs myself now (and just point AI to the original .tex files, in German).
It is hard to believe how much the models and agentic harnesses improved over the last year.
I cannot describe how much fun it is to do refactorings with AI on a verified Lean project!
Also, it's so easy now to have visualizations and typesetted documents generated by AI, from dependency visualizations of proofs using the Lean reflection API, to visual execution traces of cellular automatas.
I use VS Code in a beefy Codespace, with GitHub Copilot (Opus 4.5).
I have a single instruction file telling the AI to always run "lake build ./lean-file.lean" to get
feedback.
This is very similar to how I worked with Lean a year ago (of course in a much simpler domain) - mostly manual editing, sometimes accepting an inline completion or next edit suggestion.
However, with agentic AI that can run lean via CLI my workflow changed completely and I rarely write full proofs anymore (only intermediate lemma statements or very high level calc statements).
There have been bugs in Lean that allowed people to prove False, from which you can prove anything (they have been fixed).
Otherwise, if you check that no custom axiom has been used (via print axioms), the proof is valid.
It's easy to construct such an example: Prove that for all a, b, c and n between 3 and 10^5, a^n=b^n+c^n has no solution.
The unmeaningful proof would enumerate all ~10^20 cases and proof them individually. The meaningful (and probably even shorter) proof would derive this from Fermat's theorem after proving that one.
Over the past year, I went from fully manual mode (occasionally asking chat gpt some Lean questions) to fully automatic mode, where I barely do Lean proofs myself now (and just point AI to the original .tex files, in German). It is hard to believe how much the models and agentic harnesses improved over the last year.
I cannot describe how much fun it is to do refactorings with AI on a verified Lean project!
Also, it's so easy now to have visualizations and typesetted documents generated by AI, from dependency visualizations of proofs using the Lean reflection API, to visual execution traces of cellular automatas.