Post

Screw bug-finding, I wanna know if Mythos can handle topology (at least at noticed on its own it screwed up)

@vikramsaraph.com topology mentioned 🫨

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.

Need to write about this/resume this sometime

Not at all advocating for this (for various reasons), but I was thinking that someone could hypothetically write an MCP server that fetches context from Lean’s Zulip server, especially since it doesn’t require authentication to browse and has an API

Last I browsed there was discussion here and there about possibly adding combinatorial simplicial complexes and related things. But generally I expect there to be valuable information about writing certain proofs. It’s a very active server