Using Lean and LLMs to learn math via a toy universe

Stream: new members

[typh]

I'm an amateur math enthusiast who was drawn to Lean (via The Natural Number Game) because, well, if I can't do something in a terminal, I struggle to do it at all. I started a few projects playing with cellular automata, but I found myself more interested in understanding static structures than simulations.

I created Diaspora as an effort to explore formal structure that was compatible with my philosophical intuitions. Mainly around perspectives, constraints, novelty, creation of structure. Diaspora morphed into a toy universe built on hodge theory and graphs. So on top of being a tour through math for me, it became a tour through physics. https://github.com/typhdotcom/diaspora

It's very much an LLM-collaborated "vibe math" project, so it comes with the usual pitfalls: messy lean, naive interpretations, hallucination. Sometimes portions of it crumble. I'm ok with that- often dissecting where I went wrong is when I learn the most.

It's hard to know where to share such a project, because sharing vibe code feels kinda like sharing a dream. But I figure a new member post is low stakes, and I'm probably not the only person interested in Lean for this type of exploration.

[suhr]

Welcome! It's nice to see a project that compiles, even if it's written with an LLM.

[Jireh Loreaux]

typh said:

It's very much an LLM-collaborated "vibe math" project, so it comes with the usual pitfalls: messy lean, naive interpretations, hallucination. Sometimes portions of it crumble. I'm ok with that- often dissecting where I went wrong is when I learn the most.

It's hard to know where to share such a project, because sharing vibe code feels kinda like sharing a dream. But I figure a new member post is low stakes, and I'm probably not the only person interested in Lean for this type of exploration.

:heart: the fact that you are cognizant of these issues is a pleasant surprise compared to most AI-generated content we get here.