AI research & science

10 Nov 2026Google DeepMind says agents built on Gemini Carbon wrote about 6.5 million lines of Lean proof showing that the compiled machine code of libsignal, the Signal protocol's official implementation, meets key security guarantees: forward secrecy, post-compromise security, authentication and handshake secrecy. Humans, working with AI models, wrote and reviewed the specifications, about 26,000 trusted lines in all, and the agents flagged about 1% of the proof for human review. DeepMind says it took four weeks. To check the specifications catch real mistakes, the team reinserted two old, fixed bugs and proved those versions insecure. The paper is clear about the limits: the proofs cover Google's own command-line build rather than the Signal apps, assume perfect cryptography in the symbolic proof, and exclude side channels. The proofs are open source. Read my post.

4 Nov 2026OpenAI describes an autonomous pipeline that scans the Linux kernel for flaws, reproduces them in isolated virtual machines, tests whether they can be exploited and drafts patches, with human researchers reviewing everything before it is reported. In a mid-October run it says the pipeline reproduced 1,724 vulnerabilities and produced working exploits for 948 distinct privilege-escalation flaws, at an API cost of about $1.2 million. OpenAI says ten of the exploitation techniques were new to outside experts, and that 20 of 200 early "successes" turned out to have used a different flaw from the one assigned. These are OpenAI's figures and have not been independently checked. Read my post.

2 Nov 2026Anthropic's Frontier Red Team released FlashProve, an open-source prototype for "provable inference". A provider publishes a commitment to a model's weights and then attaches a proof to each reply, which anyone can check on an ordinary processor in seconds, without seeing the weights, to confirm that the reply came from the committed model. In a demonstration with a 400-billion-parameter open model on one H100 graphics card, Anthropic reports proofs generated at over 100 tokens a second and about 19 MB per 1,024-token request, which costs roughly 70 to 95 times the GPU time of simply processing the prompt. Parts of the protocol are machine-checked in Lean, but the authors say the programs that implement it are not proved to hide the weights.

26 Oct 2026OpenAI and Anthropic each say an internal model found, on 16 October, a proof that the Exponential Time Hypothesis is false. ETH is the assumption, used in hundreds of papers, that the classic 3-SAT puzzle cannot be solved without exponential time. Both companies published papers and Lean proofs that a computer has checked, but human review is not finished: Russell Impagliazzo, who co-proposed ETH and is helping review OpenAI's version, told Science it is "not 100% certain". The result is theoretical and does not make anything faster in practice. Read my plain-English guide.

9 Nov 2026In its Claude Fable 5.2 announcement, Anthropic says a team of about 1,000 Fable 5.2 agents formalised the proof of Fermat's Last Theorem in Lean in 30 hours, against 11 days for its first formalisation with an unreleased research model. Anthropic later clarified that the agents started with 60 target statements, a one-sentence sketch of the classical route and 47 lemmas from that earlier work. It also says Fable 5.2 solved two open problems about black holes, described in two preprints, and that Mythos 5.2 found a way to predict the structure of whole gene-therapy capsids, accurately modelling 28 of 34. These are Anthropic's claims. My post.

26 Oct 2026In the same announcement, OpenAI claimed two more results. It says its models proved the local smoothing conjecture in every dimension, which would also settle the Kakeya and Stein restriction conjectures; it released the AI output and a Lean proof as they are. It also claims a rigorous proof that certain four-dimensional quantum field theories exist, including quantum chromodynamics and pure Yang–Mills theory, part of a Millennium Prize problem. A group led by Nobel laureate David Gross is reviewing that work and has chosen to hold back the material for now. These are OpenAI's claims and remain under expert review.

21 Oct 2026Microsoft Research says Xinzhi Zhang and Zhao Song have proved the Kannan–Lovász–Simonovits (KLS) conjecture, a question in high-dimensional geometry open since 1995. The researchers directed AI agents that explored more than 100 possible approaches, while the people set the direction and checked the proof. Microsoft says AI runs left to work alone on a similar budget fell short. It also notes other independent proofs and a formalisation in the Lean proof assistant. As with any new proof, the final word belongs to peer review.

27 Oct 2026Google DeepMind announced Genie 4, a model that generates interactive worlds in real time, now with native audio and interactive dialogue, guided by Gemini 3.8 Flash. It is a research preview for trusted testers and will reach Google AI Ultra subscribers in Project Genie and early-access partners of the Gemini API and AI Studio first. Outputs carry SynthID watermarks. DeepMind lists drift over time and keeping track of objects as current limitations.

10 Nov 2026The Institute of Foundation Models released PAN 2, an open world model that turns a starting scene and a described action into a video of what happens next. Unusually, it comes with full training code as well as weights, under Apache 2.0. IFM says it placed third on the Physics-IQ Verified leaderboard and first among open-weight models.

22 Oct 2026Anthropic and Theorem report that Claude wrote machine-checked proofs, in the Rocq proof language, that 239 entry points across 123 open-source libraries cannot crash on inputs under 64 MB. The proofs total about 180 million lines and turned up hundreds of bugs along the way. The results hold only under stated assumptions, such as single-threaded RISC-V builds, and Anthropic stresses that "formally verified does not mean bug-free". Read my post on AI and software security.