Ken Ono
@KenOno691
Founding Mathematician @axiommathai | Prof @UVA | AI, proof | Assoc. Producer, The Man Who Knew Infinity | Olympic swim performance 🏊♂️🏅
参加 March 2024
193 フォロー中 67.1K ファン
We gave AxiomProver a real-world stress test: autoformalizing Theorem 1.2 from Yifeng Huang's latest paper. This isn't vanilla theory; it’s a gnarly quadratic form generalization involving gap posets and rational dinv.
I couldn't crack this proof myself. So pleased that AxiomProver formalized it Lean/Mathlib. This is a glimpse of the future. Mahalo @leanprover
もっと見る
