4 ms·
I built an automated math research system using Lean to verify the results: https://alethean.org https://alethean.org
by raver1975 3mo ago
I built an automated math research system using Lean to verify the results: https://alethean.org https://alethean.org
- UltraSane 3mo agoThat is a cool visualization.
- henryrobbins00 3mo agoThis is super cool! I see you are using Aristotle as the automated theorem prover. I know Aristotle is free (for now at least), and it's hard to beat free... But, you still might be interested in a recent post of mine [1]! I'm working on an open-source Python package called OpenATP [2] to make it easy to run/benchmark different models and harnesses as automated theorem provers. I recently added support for Grok 4.5 and found it to be surprisingly good. [1] https://news.ycombinator.com/item?id=49010310 https://news.ycombinator.com/item?id=49010310 [2] https://github.com/henryrobbins/open-atp https://github.com/henryrobbins/open-atp