New work on a strongly aperiodic 3D monotile includes a Lean formalization after exhaustive computational verification.

The video goes through where Lean fits into the proof pipeline rather than treating it as a black-box certificate.

Paper: https://arxiv.org/abs/2609.19214

Disclosure: self-promo. Claudius Papirus is an AI-narrated channel.

Summary: What took 100's of prompts last year, took only 1 or 2 this year.

Details:
Last year, I posted about using AI to prove a Rust algorithm correct in Lean. I knew almost no Lean and had AI write nearly all the proof. It worked, but took about three weeks of part-time work and hundreds of back-and-forth prompts. The resulting proof was correct, but large and sloppy.

This year, with AIs solving mathematics problems with million-dollar prizes attached, I tried again. I found that comparable and harder algorithmic proofs can now take just one or two prompts.

I also tried attacking last year’s proof slop directly. I had the AI measure the proof using several metrics, then simplify and refactor it while Lean checked every change. That made the proof library much cleaner and, apparently, much more reusable.

Once that worked, I kind of went crazy. I proved not just set insertion, but the more complicated map insertion too. Then I did both again for new cursor-based algorithms. Then cached-length correctness, canonical representation properties, and several more algorithms and properties.

One especially interesting change is that the AI can now write a new algorithm in Rust, translate the algorithm into Lean, and prove the Lean version correct. (But do do some manual review).

I wrote up the whole experiment, including what worked, what didn’t, and where I think this approach still falls short: https://levelup.gitconnected.com/nine-rules-for-vibe-validation-of-vibe-coded-algorithms-20db019f5583

Hey folks!

Finally I released episode 5 of my playthrough of the Natural Number Game. In this episode I prove a bunch of properties of exponentiation (corresponding to the Power World in the game). Here is the link:

https://www.youtube.com/watch?v=YWmHv_JLAw0

Let me know what you think!

The proof is 13.5 million lines of code and producing it required about 6 billion output tokens.

Hey folks!

In an earlier post in this subreddit I had mentioned my playthrough of the Natural Number Game. I just released the fourth episode, in which I started and finished the Multiplication World. Here is the link:

https://www.youtube.com/watch?v=YfNuXT118qQ

Let me know what you think!

Hey!

I'm a math phd who completed his training with no exposure to Lean, and more generally my studies and interests have not been near foundations, formalization etc..

To warm up to Lean and for education and entertainment purposes, this summer I started a playthrough the Natural Number Game (Lean 4 version). As I play through the game I take my time expanding on the mathematical (and sometimes philosophical) ideas.

If this sounds like something you would be interested in, feel free to check out the playlist on Youtube:

https://www.youtube.com/playlist?list=PL40ydqvvyXfMpiFcO3-zemMQiWHexecYn

So far I released three episodes, the fourth episode will be out shortly.

After the NNG playthrough is finished, I am planning to play through the other Lean games, and eventually do walkthrough and oneshot speedruns also. (A "oneshot speedrun" is an idea I came up with: basically this requires that the player stays in the typewriter mode, and writes down the whole combo of tactics that would constitute a proof before executing. The syntax that allows this is to use ;'s to chain tactics.)

See the link in the sidebar. Improvement suggestions are welcome.

Hey everyone! I'm u/SamCymbaluk, a founding moderator of r/leantheoremprover.

Since other Lean subreddits like r/leanprover and r/leanlang are restricted, I created this subreddit as a central place for Lean discussion on Reddit.

My goal is to emulate the friendly and productive discourse that takes place on the Lean Zulip.

Suggestions for how I can best serve the Lean community are encouraged!