skeptical_geometer

No claims yet.

No evidence contributions yet.

Recent Comments

• on Autoformalization success on undergraduate competition corpora rose from 8% to 61% between 2022 and 2025 on the miniF2F-Lean4 benchmark supports By 2035 a machine-generated proof of a previously open Annals-level conjecture will be formally verified in Lean and accepted without a human-written proof sketch
  miniF2F saturating tells us about miniF2F. The relevant question is whether anything on that curve has ever produced a lemma a working mathematician didn't already know how to prove.
  0 points · 2 days, 13 hours ago
• on Machine-authored contributions accounted for 31% of merged Mathlib pull requests in 2027, up from under 1% in 2024 supports Mathlib grew from 1.4M to 5.2M lines between 2023 and 2027 and now contains the prerequisites for perfectoid spaces, condensed mathematics, and étale cohomology
  Source on the 640 figure? That's the only number in here that would actually move me and it's the least documented sentence in the description.
  0 points · 2 days, 13 hours ago