Post

I tried this again 6 months later. Claude Code got *way* farther this time (though I did use Opus 5.x): github.com/vhxs/simplic... I have the simplicial approximation theorem. The definitions are compatible with already exists in Mathlib. It took shockingly little input from me...

github.comGitHub - vhxs/simplicial_complexesContribute to vhxs/simplicial_complexes development by creating an account on GitHub.

Vikram Seraph 🪽@vikramsaraph.com

Sonnet 4.5 got surprisingly far with proving the simplicial approximation theorem in Lean. I was trying to define combinatorial simplicial complexes in such a way that the geometric realization functor uses the existing definition of geometric complexes already in Lean’s mathlib.

Vikram Seraph 🪽

@vikramsaraph.com

... though there were some important decision points where I had to provide input. I didn't have to fight CC to break down proofs into manageable lemmas, it did that all on its own (last time it would blow through my token budget if I wasn't careful)

27/10/26, 1:53 am0 reposts0 likes

Vikram Seraph 🪽

@vikramsaraph.com

It doesn't look like any of this is in Mathlib (yet anyways). I used CC to look for other existing Lean proofs out on the internet; didn't find much.

Vikram Seraph 🪽

@vikramsaraph.com

There was this related paper: Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean drops.dagstuhl.de/storage/00li... published here: itp-conference-2026.github.io/index.html

itp-conference-2026.github.ioITP 2026ITP 2026 is the seventeenth conference on Interactive Theorem Proving and related issues, ranging from theoretical foundations to implementation aspects to ap...

Vikram Seraph 🪽

@vikramsaraph.com

in searching, I also came across this odd website/project: taucetiproject.org In CC's words: "a Lean library downstream of Mathlib where AI agents implement against human-written roadmaps."

taucetiproject.orgTau Ceti — Tau Ceti

Vikram Seraph 🪽

@vikramsaraph.com

So much of this was done passively while I was working on other things. Eventual goal is the asynchronous computability theorem and related results.