Gauss just autoformalized the proof of the Kakeya conjecture for finite fields! (1/5)

The Kakeya conjecture was originally posed in 1917. It was solved in 2 dimensions almost 100 years ago. But just this year in 2025, Wang & Zahl solved it for 3 dimensions. (2/5)

The Kakeya conjecture for finite fields was solved in all dimensions simultaneously by Dvir in 2008. Dvir’s proof came as a shock to the math world. (3/5)

Before, both Terence Tao (Fields medal 2006) and Jean Bourgain (Fields medal 1994) had been stuck making minor improvements on the problem for years. At the time, Dvir was just a PhD student! (4/5)

And the proof Gauss wrote was surprisingly efficient, in just 6 hours! https://github.com/math-inc/KakeyaFiniteFields… If Dvir had access to Gauss, he could have published his breakthrough proof, with a certification of correctness in real time. (5/5)