Hacker News: marwahaha

New comment by marwahaha in "Formalizing Fermat's Last Theorem"

marwahaha — Sat, 05 Sep 2026 08:36:28 +0000

I helped build https://prove2.me . It's not proof-specific but everything is Lean-based. I've found the tool useful when formalizing recent upper bounds on $\omega$ (in computational complexity of matrix multiplication). A lot of ideas in this tool are experimental, but the intent is to benefit the mathematical community at large. I'd be happy to hear about any suggestions or advice others have.

New comment by marwahaha in "Formalizing Fermat's Last Theorem"

marwahaha — Sat, 05 Sep 2026 08:28:49 +0000

I was involved in building https://prove2.me (but I am not affiliated with Anthropic nor involved in anything related to FLT). I think the key insight in prove2me is to prove theorems "top-down", which allows a large number of users to collaboratively work on a single theorem statement. This setup also seems to work well for a "swarm" of agents. I posted more of my thoughts on the Lean Zulip.

New comment by marwahaha in "My collection of machine learning paper notes"

marwahaha — Thu, 22 Apr 2021 10:43:16 +0000

Sure, I built one. I think it will work if you keep your paper collection page in the same format.

https://github.com/arxivwiki/kurin-paper-scraper https://github.com/arxivwiki/arxivwiki/blob/main/.github/wor... https://github.com/arxivwiki/arxivwiki/blob/main/.github/wor...

New comment by marwahaha in "My collection of machine learning paper notes"

marwahaha — Wed, 21 Apr 2021 22:14:13 +0000

I really like this. I recently started a similar project called the "arXiv wiki". Could you link future paper notes here?

For example: https://arxiv.wiki/abs/2101.06861

New comment by marwahaha in "Help College Students Ace Technical Interviews"

marwahaha — Wed, 17 Mar 2021 10:19:31 +0000

It's a nonprofit: https://codepath.org/about

Help College Students Ace Technical Interviews

marwahaha — Wed, 17 Mar 2021 00:10:06 +0000

Article URL: https://info.codepath.org/summer-technical-mentor

Comments URL: https://news.ycombinator.com/item?id=26484943

Points: 1

# Comments: 2

New comment by marwahaha in "Show HN: Wordcloud Generator from ArXiv Abstracts"

marwahaha — Thu, 11 Mar 2021 21:11:48 +0000

I'm applying to graduate programs this cycle; this tool helped give me a vague idea of a professor's research interests without reading through their papers. What do you think?

Show HN: Wordcloud Generator from ArXiv Abstracts

marwahaha — Thu, 11 Mar 2021 09:15:18 +0000

Article URL: https://marwahaha.github.io/arxiv-wordcloud/?author=Boaz%20Barak

Comments URL: https://news.ycombinator.com/item?id=26421965

Points: 1

# Comments: 1

New comment by marwahaha in "Show HN: Where is the “average” person in each US state?"

marwahaha — Mon, 11 Jan 2021 06:52:54 +0000

Thanks. I made an issue to track this: https://github.com/marwahaha/ca-center/issues

New comment by marwahaha in "Show HN: Where is the “average” person in each US state?"

marwahaha — Fri, 08 Jan 2021 11:19:39 +0000

Thanks! I did so.

Show HN: Where is the “average” person in each US state?

marwahaha — Fri, 08 Jan 2021 09:00:42 +0000

Article URL: https://marwahaha.github.io/ca-center/viewer

Comments URL: https://news.ycombinator.com/item?id=25682905

Points: 6

# Comments: 4