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 🫨

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