#proofassistants

Epoch lists its Apéry irrationality target as solved “human + AI” after a September preprint claimed ζ(5) is irrational and linked public Lean formalization, while independent mathematical review and the AI attribution remain unresolved.

An unreleased research version of Claude raised the proven lower bound on the fraction of Riemann zeta zeros lying on the critical line from 41.6 percent to 67.2 percent, and Anthropic published the paper and a machine-checked Lean proof on August 10

Mathematicians found an explicit counterexample disproving the Jacobian conjecture in three dimensions, checked partly with an AI chatbot and formalized in a Lean proof, while two other viral AI-math claims remain unverified.