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

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