AI Briefing#lean
The latest AI and developer news about #lean, with the original source and a short summary.
The latest AI and developer news about #lean, with the original source and a short summary.
The 30-hour proof used about a third of the action tokens and was roughly 7x shorter than the 11-day September run.
The multi-LLM agentic framework generated over six million lines of Lean code to mathematically prove the security of the actual Signal code in four weeks.
The proof, verified by Lean, establishes that quantum computers cannot achieve exponential speedups on random inputs without specific structural patterns.
The 16 million-line library is the largest integrated formalized mathematics collection, enabling direct import of algebraic geometry definitions and theorems.
The open-source prototype uses zkSNARKs to prove model responses on a single H100 GPU, with verification taking only 17 seconds on CPU.
The October 28 update includes support for Tau Ceti's open Lean maths library and FlyWire's brain-mapping tools.
The 24-day formalization generated 43.1 million lines of code and identified 34 significant discrepancies in existing mathematical proofs.
OpenAI released AI-generated proofs for the local smoothing conjecture and a refutation of the Exponential Time Hypothesis, while deferring the release of physics results to external expert collaborations.
Basis Research used LLMs to write formal semantics for an extended WHILE language and prove in Lean that its compiled C interpreter's RISC-V binary execution matches those semantics.
Tao argues that AI's ability to mechanically verify and generate proofs requires decentering problem-solving to preserve human understanding and long-term mathematical health.
Researchers argue that semantic ambiguities in natural language make faithful AI autoformalisation computationally harder than the Halting problem, undermining confidence in the verification of OpenAI's claimed Navier-Stokes blow-up proof.
OpenAI has released new mathematical results from an internal frontier model, including Lean formalizations and compute estimates averaging three hours of ChatGPT Pro usage.
The proof was posted in a pinned GitHub commit on August 28, coinciding with a Fields Medalist's essay predicting AI would solve the problem before humans.
AI agents generated an LSP server, decompiler, and 95 Lean correctness proofs over six months, uncovering a high-severity vulnerability that could allow fund theft.
Anthropic has published the first fully mechanically verified proof of Fermat's Last Theorem using Claude.
Claude autonomously formalized Fermat's Last Theorem in the Lean language in just 11 days, generating 13 million lines of code.
Anthropic successfully formalized Fermat's Last Theorem into a computer-verifiable format in 11 days using Claude and the Prove2Me platform.
LLM-powered automation is shortening the formal verification process, a core aspect of programming language research, and changing research culture.
Claude raised the lower bound for the proportion of zeros of the Riemann zeta function on the critical line to 67.2%.
OpenAI's unreleased model Astra has produced new results on 10 open math problems.
OpenAI has released new results on 10 long-unsolved problems in mathematics and theoretical computer science.
Fuzzing of Lean-verified code uncovered a runtime overflow and a DoS vulnerability.
105M fuzzing runs uncovered a Lean runtime heap overflow and a lean-zip DoS.
A 2-week sprint isn't the right answer for everyone; the cadence that fits your team's situation matters more.