Testing shows that code works for the inputs you tried. Formal verification aims to show it works for every input within defined limits, by writing a proof that an independent checker can confirm step by step. It has traditionally been very expensive and reserved for safety-critical code such as avionics or operating-system kernels. A proof is only as strong as its assumptions: it covers the stated hardware, configuration and input sizes, and says nothing outside them.
NLP & LLMsResearch
Lean explained: how AI agents turn math proofs into checked code
Anthropic says Fable 5.2 agents formalized Fermat's Last Theorem in Lean in 30 hours. Here is what Lean is, what formalization means and what the claim does not show.
thelatentdaily.com Editorial Team5 min read
