Can AI do maths yet? Thoughts from a mathematician.

My feed was recently clogged up with news articles reporting that Sam Altman thinks that AGI is here, or will be here next year, or whatever. I will refrain from giving even more air to this nonsense by linking to … Continue reading →

So I'm two months into trying to teach a proof of Fermat's Last Theorem to a computer. We already have one interesting story, which I felt was worth sharing. Continue reading →

A huge amount happened in the Lean theorem prover community in 2023; this blog post looks back at some of these events, plus some of what we have to look forward to in 2024. Modern mathematics I personally am a … Continue reading →

(This is a guest post by Bhavik Mehta) On March 16, 2023, a paper by Campos, Griffiths, Morris, and Sahasrabudhe appeared on the arXiv, announcing an exponential improvement to the upper bound on Ramsey numbers, an open problem since 1935. … Continue reading →

A brief survey post containing some of the things which happened in the Lean community in 2022. The Liquid Tensor Experiment In December 2020, Fields Medallist Peter Scholze challenged the formal computer proof community to verify one of his theorems … Continue reading →