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

Wes Pegden @wespegden.bsky.social · 15/12/2024

In fairness, it's a funny joke, and I think that may be all it is (rather than, say, a serious call to end math education).

130

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 · 25/11/2024

With data like this there's a Q of whether what you're seeing is really people being "wrong" about proportions vs not having enough numeracy for the concept to even be meaningful. If you ask enough state residency questions in this survey you're on track to have 1000% of the US pop living somewhere.

020

Wes Pegden @wespegden.bsky.social · 23/11/2024

What is your ideal format for a rain forecast?

010

Wes Pegden @wespegden.bsky.social · 23/11/2024

I'd be really interested in seeing your longer take on meteorology. For everything from hurricane landing probabilities to the probabilities of rain on Tuesday, these are forecasts that I think most people don't have any doubt have utility. Very curious to see the best argument against it!

110

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

Few people covered themselves in glory in this timeperiod. The GBD was not great but it was not scientifically nonsensical. E.g. from a science standpoint the John Snow memo was arguably worse and if we impune everyone who signed either of these documents, few are left standing.

010

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