FVSpec Turns Real-World Property-Based Tests into Lean Verification Challenges

A new arXiv preprint introduces FVSpec, a benchmark that repurposes property-based tests drawn from real software projects as proof challenges in the Lean theorem prover. The work targets the growing need to verify machine-generated code, arguing that AI systems themselves could take on much of that verification work. It also notes that the field still lacks a clear picture of how well current tools and models handle such tasks.

StochBench: A Lean 4 Benchmark for Stochastic Processes in Formal Theorem Proving

Researchers have released StochBench, a Lean 4 benchmark containing 45 problems centered on stochastic processes. It was created because existing evaluations of language models in formal theorem proving rely heavily on small sets of competition-style problems, which do not reflect how such models perform on domain-specific mathematical fields.

Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

A new arXiv paper introduces Magenta, a method that connects informal natural-language mathematical reasoning by large language models with the formal proof assistant Lean. The approach aims to let models generate reasoning in ordinary language while Lean checks correctness, closing the gap between informal and formally verified mathematics.

OpenAI claims Navier-Stokes proof generated by 10,000-agent system

OpenAI says a system of 10,000 agents produced a proof addressing one of the Millennium Prize problems, Navier-Stokes. The result was published alongside a Lean repository to support independent verification and concerns a particular case covered by the official problem statement. The validity of the proof remains under scientific review.

OpenAI shares AI-generated solution to Navier–Stokes Millennium Prize problem with Lean proof

OpenAI says its AI has produced a solution to the Navier–Stokes problem, one of the Clay Mathematics Institute's seven $1 million Millennium Prize challenges. The release includes a technical writeup together with a machine-checked formal proof written in the Lean proof assistant. Whether the argument constitutes a complete, correct solution will depend on scrutiny from the mathematics community.

WHY IT MATTERS ↘Pairing a frontier-model claim with a machine-checked Lean proof shifts verification from trusting the lab to auditing a formal artifact, a template that could become standard for evaluating AI reasoning claims. It also escalates competitive pressure among labs to target landmark open problems, though expert scrutiny of the argument remains the real bottleneck before any practical or prize implications follow.