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.

Interest in software verification has surged, with a notable increase in Google Trends searches for formal verification and formal methods over the past two years. Many engineers are now learning Lean and exploring new specification languages, indicating a growing excitement around the topic.

Leanstral 1.5 is a free Apache-2.0 licensed model with 6 billion active parameters that significantly enhances performance in formal verification. It solves 587 out of 672 PutnamBench problems, achieves state-of-the-art results on FATE-H (87%) and FATE-X (34%), and uncovers five previously unknown bugs across 57 repositories.

The cost and tooling of formal verification have become widely accessible, allowing for increased use in software development. AI is reducing the barriers to formal verification by eliminating the costs associated with writing proofs, enabling the creation of software that guarantees mathematically correct business rules.

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.