Lean 4: How the theorem prover works and why it's the new competitive edge in AI

Yes, though often the easiest way to replicate it in regular programming languages is to translate that language to Lean or another ITM, though auto-active like Verus is used for Rust pretty successfully.

Python and C though have enough nasal demons and undefined behavior that it's a huge pain to verify things about them, since some random other thread can drive by and modify memory in another thread.

Yes exactly. There is this thing called the “Curry-Howard Isomorphism” which (as I understand it) says that propositions in formal logic are isomorphic to types. So the “calculus of constructions” is a typed lambda calculus based on this that makes it possible for you to state some proposition as a type and if you can instantiate that type then what you have done is isomorphic to proving the proposition. Most proof assistants (and certainly Lean) are based on this.

So although lean4 is a programming language that people can use to write “normal” programs, when you use it as a proof assistant this is what you are doing - stating propositions and then using a combination of a (very extensive) library of previous results, your own ingenuity using the builtins of the language and (in my experience anyway) a bunch of brute force to instantiate the type thus proving the proposition.

The real value is in mixed mode:

- Lean supports calling out as a tactic, allowing you to call LLMs or other AI as judges (ie, they return a judgment about a claim)

- Lean can combine these judgments from external systems according to formal theories (ie, normal proof mechanics)

- an LLM engaged in higher order reasoning can decompose its thinking into such logical steps of fuzzy blocks

- this can be done recursively, eg, having a step that replaces LLM judgments with further logical formulations of fuzzy judgments from the LLM

Something, something, sheaves.

Lean is a great idea, especially the 4th version, a huge level up from the 3rd one, but its core still deficient[1] in some particular scenarious (see an interesting discussion[2] in the Rock (formerly Coq) issue tracker). Not sure if it might hinder the automation with the AI.

[1] https://artagnon.com/logic/leancoq

[2] https://github.com/rocq-prover/rocq/issues/10871

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.