Wes Pegden

Trellis has formalized the Strong Perfect Graph Theorem of Chudnovsky, Robertson, Seymour, Thomas. It ran autonomously for 6 weeks; the proof is 540k LOC, the largest Lean autoformalization. OG paper here: annals.math.princeton.edu/2006/164-1/p02 Viewer, git here: math.cmu.edu/~wes/trellis...

Just posted manuscript and code for Trellis, an autoformalization system that aims to take a math paper in LaTeX and output a complete formalization in Lean. Link has pretty viewers with formalizations of recent Ramsey theory breakthroughs. www.math.cmu.edu/~wes/trellis... arxiv.org/abs/2606.09674

Learned on MathOverflow: it is possible to write a finite formula for n! involving just the operations of addition, subtraction, multiplication, integer division, and exponentiation. Precise statement is here: mathoverflow.net/a/484115/17064

I think this is my favorite paper title so far: "Youden's demon is Sylvester's problem" arxiv.org/abs/2407.02589