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...

... 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)

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.

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."