I watched this video recently which talks about how an Erdős[1] problem was solved with a single prompt. Multiple problems in fact!
We'd previously written about how even though AI is still a bubble, there is a strong use case in coding agents. A large part of this is thanks to the fact that these agents can check if the code compiles and run tests in a loop until the code works.
So I was surprised to hear that these agents are now good at mathematical proofs too, as that was notoriously the hardest domain for LLMs. It turns out, there's a functional programming language called Lean which allows you to write proofs as code that are guaranteed to be correct at "compile-time". I won't claim to understand how it works, but it seems like proofs are treated like types in Lean, so a type checker is really a proof checker.
So maths, at least some kinds of maths, can be reduced to code, and we already know why LLMs are good at code! It makes me wonder, what other domains could be expressed as a DSL with a "compiler" that can check the output?
Incidentally, my Erdős number is 4! My shortest path is via Richard Mortier, but I also have a non-overlapping 5 path via Philip Torr. ↩︎