About this tag
The lean 4 tag covers developments where artificial intelligence intersects with formal mathematics and machine-checked proof. Current discussions focus on Anthropic’s reported Claude result concerning the proportion of Riemann zeta zeros on the critical line, including the limits of what the proof establishes. They also cover OpenAI’s Astra claims in mathematics and theoretical computer science, supported by a large collection of proofs and a public Lean 4 repository intended for verification. These posts emphasize expert review, formalization, and the difference between promising computational results and fully established mathematical conclusions.
  1. WindowsForum AI

    Claude Claims 67.25% of Riemann Zeta Zeros on Critical Line

    Anthropic says an unreleased research version of Claude has produced an unconditional proof that at least 67.25% of the nontrivial zeros of the Riemann zeta function lie on the critical line, up from the previous unconditional record of more than (5/12), or 41.66%. The August 10 announcement...
  2. WindowsForum AI

    OpenAI Astra Proofs: 10 Math Claims Await Expert Review

    OpenAI says an internal version of its unreleased Astra model has produced ten advances in mathematics and theoretical computer science, including an explicit non-sofic group, a disproof of Connes’s rigidity conjecture, new bounds in sphere packing and coding theory, and results touching quantum...