iiinova — where your digital self keeps evolving

Wes Pegden

@wespegden.bsky.social

Mathematician, CMU

Wes Pegden @wespegden.bsky.social · 02/09/2026

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...

021

Wes Pegden @wespegden.bsky.social · 10/06/2026

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

math.cmu.edu

Trellis

Trellis.

030

Reposted by Wes Pegden

Gro-Tsen @gro-tsen.bsky.social · 14/12/2024

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

Screenshot of an answer by Emil Jeřábek on MathOverflow that contains, among other things, a formula for the factorial of n using addition, subtraction, multiplication, integer division and exponentiation, and a reference to the fact that any Kalmár elementary function can be similarly expressed.

3368

Wes Pegden @wespegden.bsky.social · 17/09/2024

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

arxiv.org

Youden's Demon is Sylvester's Problem

If four people with Gaussian-distributed heights stand at Gaussian positions on the plane, the probability that there are exactly two people whose height is above the average of the four is...

130