lean
Latest stories covering lean, with summaries and links to related coverage.
3 articles · page 1 of 1
Connected topics
Palomar: A registry of Lean verified mathematics
research
3 min read
Palomar, a registry for Lean-verified mathematics incubated by the Lean FRO and ICARM, has opened for submissions. It records fixed GitHub repository snapshots containing formal Lean proofs of old or new mathematical results, including work produced by humans, AI systems, or both. Terence Tao serves on its scientific advisory board alongside Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh. Each submission must include a challenge file that states the claimed results in human-readable Lean, a solution module containing proofs, and a formalization.yaml metadata file with an informal description and disclosures. Palomar mechanically uses Lean Comparator to verify that the solution typechecks and proves the challenge file’s statements. A large language model separately assesses whether the informal description appears to match those formal statements, while the registry also checks minimal repository standards. Registration does not constitute peer review for novelty, interest, or mathematical accuracy. Tao reported successfully submitting his recent Lean formalization of the proof of Sendov’s conjecture as a test and plans to submit older formalizations. AI agents can assist with submission mechanics, though Palomar recommends human review.
We have proof automation now
opinion
18 min read
ImperialViolet discusses the advantages of dependently-typed languages like Coq, Rocq, and Lean for enforcing complex invariants through their type systems. These languages help prevent misunderstandings and integration issues in large teams by formally encoding requirements that might otherwise be lost.
Lean proved this program correct; then I found a bug
opinion
7 min read
AI agents are increasingly effective at identifying vulnerabilities in large software systems. Anthropic chose not to release the Mythos model due to concerns over its potential to discover dangerous security flaws.