Papers
Browse papers, Lean formalisations and published audits.
- A quadratic form generalization of rational dinv — Yifeng HuangLean repository linked
- A streamlined proof of the Kakeya set conjecture in ℝ³ — Larry Guth, Hong Wang, Joshua ZahlLean repository linked
- A Vertex-Localized Positive Square-Energy Strengthening of Turán's Theorem — Abhay Jayarajan, M. Rajesh Kannan, Shivaramakrishna Pragada, Rahul RoyLean repository linked
- ABC implies that Ramanujan's tau function misses almost all primes — David Kurniadi Angdinata, Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Simon Mahns, Aram H. Markosyan, Rithikesh Muddana, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian ZhangLean repository linked
- Almost all orbits of the Collatz map attain almost bounded values — Terence TaoLean repository linked
- Almost all primes are partially regular — Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian ZhangLean repository linked
- An Exact Distribution-Free Test for Means of Nonnegative Random Variables — Nikos Vlassis, Philip S. ThomasLean repository linked
- Fel's Conjecture on Syzygies of Numerical Semigroups — Evan Chen, Chris Cummins, GSM, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian ZhangLean repository linked
- Finite time blowup for Navier–Stokes — OpenAIAudit published
- Finite time blowup for the Euler equation — OpenAILean repository linked
- Formalization of Brownian motion in Lean — Rémy Degenne, David Ledvinka, Etienne Marion, Peter PfaffelhuberLean repository linked
- Four-digit Kaprekar dynamics in odd bases — Evan Chen, Ken Ono, Richard E. Schwartz, Dinesh S. ThakurLean repository linked
- Improved Exponent for Marton's Conjecture in 𝔽₂ⁿ — Jyun-Jie LiaoLean repository linked
- Lower bounds in the polynomial Szemerédi theorem — Khalid YounisLean repository linked
- Marton's Conjecture in abelian groups with bounded torsion — W. T. Gowers, Ben Green, Freddie Manners, Terence TaoLean repository linked
- MIP*=RE — Zhengfeng Ji, Anand Natarajan, Thomas Vidick, John Wright, Henry YuenLean repository linked
- On a conjecture of Marton — W. T. Gowers, Ben Green, Freddie Manners, Terence TaoLean repository linked
- On a maximal anti-Ramsey conjecture of Burr, Erdős, Graham, and Sós — Matija Bucic, Kaizhe Chen, Jie MaLean repository linked
- On the paucity of lattice triangles — David Kurniadi Angdinata, Evan Chen, Ken Ono, Jesse Thorner, Jiaxin Zhang, Jujian ZhangLean repository linked
- Optimality of Gerver's Sofa — Jineon BaekLean repository linked
- Parity of k-differentials in genus zero and one — Dawei Chen, Evan Chen, Kenny Lau, Ken Ono, Jujian ZhangLean repository linked
- Sharp small-deviation inequalities for sums of independent nonnegative random variables — Weibo Fu, Yanjun Han, Guanyang Wang, Jun Yan, Peng Zhang, Zhengqing ZhouLean repository linked
- Superdiffusion and anomalous regularization in self-similar random incompressible flows — Scott Armstrong, Ahmed Bou-Rabee, Tuomo KuusiLean repository linked
- The sum-product conjecture is false for real numbers — Thomas F Bloom, Will Sawin, Carl Schildkraut, Dmitrii ZhelezovLean repository linked
- Uniformization of Riemann surfaces revisited — Cipriana Anghel, Rares StanLean repository linked
- Well-posedness of fully coupled McKean-Vlasov FBSDEs with jumps under full-tuple law dependence — Chunrong Feng, Christian GarryAudit needs attention