I was doing some research for a talk and came across this website for recording AI results on math problems: https://matharena.ai/ LLMs have been getting better and better at solving math problems but there is a worry that all they do is regurgitate what . . . Read more

This Github repo contains the proof that there are $2^{12} \times 3^{8} \times 8! \times 11!$ Rubik’s cubes: https://github.com/vihdzp/rubik-lean4 What! This is the most amazing thing I’ve read in a long time. What is t . . . Read more

Terry Tao posted on Mastodon that he found a bug in a proof in one of his papers thanks to trying to formalize it in Lean. This is an excellent use case of Lean and tbh the only one tha . . . Read more

This looks like a really cool tool for visualizing proofs in Lean: https://github.com/Paper-Proof/paperproof https://lakesare.brick.do/lean- . . . Read more

I came across two LLM based tactics for Lean llmstep: [L]LM proofstep suggestions in Lean LeanInfer: Neural Network Inference in Lean 4 They both use [LeanDoj . . . Read more

This was posted a while back on the Lean Zulip: LeanDojo LeanDojo: Theorem Proving with Retrieval-Augmented Language Models According to their description, LeanDojo is an open-source Lean play . . . Read more

I have always wanted to learn tactics writing in Lean. But for whatever reason, none of the tutorials that exist online have been helpful. I suspect that the best way to learn to write tactics to play around and modify the existing ones. I came across this short, 4-page tactics tutorial that look . . . Read more

An improved search engine for Lean: https://loogle.lean-fro.org/ https://github.com/nomeata/loogle I haven’t used it yet but it looks promising. I personally don&rs . . . Read more

I gave an hour long talk at the NU Math Club yesterday about Lean and theorem proving. Things that went well It w . . . Read more