henryrobbins00

6 ms·

1. 1.▲
   Dynamic Documents as Personal Software (Geoffrey Litt)(youtube.com)

   2 points by henryrobbins00 5d ago|0 comments
2. 2.▲
   by henryrobbins00 11d ago

   Michael Clarkson teaches OCaml at Cornell. I highly recommend his free course materials [1]. He’s an excellent educator. Learning functional programming paradigms had a major influence on how I design programs. Clarkson also taught snippets
3. 3.▲
   by henryrobbins00 12d ago

   Back in February, I was talking with my PhD advisor about using Lean to formally verify automated optimization modeling outputs. It eventually turned into this paper [1]. It’s been truly incredible to see how much the frontier models have p
4. 4.▲
   by henryrobbins00 14d ago

   Thanks for the recommendations. Horse-Drawn Tools and the Doctrine of Labor Saving is a very short Berry essay and particularly relevant to this conversation.
5. 5.▲
   by henryrobbins00 14d ago

   I'm afraid I won't do this justice, as it's been a while since I've thought deeply about these ideas, but here is an attempt! For me, Pirsig put it best: "Quality is the goal of Art." I too struggled to underst
6. 6.▲
   by henryrobbins00 14d ago

   I can't believe I haven't read this already. Can't wait.
7. 7.▲
   by henryrobbins00 14d ago

   I read The World-Ending Fire (Wendell Berry), Hackers (Steven Levy), and Zen and the Art of Motorcycle Maintenance (Robert Pirsig) around the same time. I was struck by how similar Berry, Pirsig, and the early MIT hackers thought about Qual
8. 8.▲
   by henryrobbins00 16d ago

   This is awesome. It reminds me a lot of the excellent work done by the Center for Land Use Interpretation (CLUI) [1]. One of my personal favorites is Pavement Paradise [2] documenting American parking spaces. I'll also shamelessly plug
9. 9.▲
   Flare: Verifying MILP Reformulations with LLM-Based Theorem Proving(arxiv.org)

   2 points by henryrobbins00 21d ago|0 comments
10. 10.▲
    by henryrobbins00 2mo ago

    I'm very bullish on proof automation as well. I'm currently researching AI for algorithm design and using automated theorem provers to get formal guarantees for generated algorithms. To make a shameless plug, I'm working on a
11. 11.▲
    by henryrobbins00 2mo ago

    This 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 wor
12. 12.▲
    by henryrobbins00 2mo ago

    If you're excited about the relationship of Lean4 to LLMs/AI (like I am), you might find my recent post interesting [1]. TL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To m
13. 13.▲
    by henryrobbins00 2mo ago

    Some additional details about these results that didn't make it into the main post: - The OpenATP "standard provers" were used; see docs [5] for model / harness configuration details - Time and cost are function of effor
14. 14.▲
    Grok is a surprisingly good automated theorem prover

    3 points by henryrobbins00 2mo ago|1 comments
15. 15.▲
    by henryrobbins00 3mo ago

    Earnest question: any recommendation to not come off this way in forums? I created this tool for my own research and have found it really helpful to benchmark different automated theorem provers (my experience so far has been that Claude Co
16. 16.▲
    by henryrobbins00 3mo ago

    Try out Leanstral 1.5 on the latest version of OpenATP! OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It natively supports running provers locally in Docker or remotely in Modal sandboxes. GitHub:
17. 17.▲
    by henryrobbins00 3mo ago

    Really? I get a 403 that I must enable Lab models on https://admin.mistral.ai/plateforme/privacy . When I try to do that, it gives "There was an error trying to update the Labs setting." Do you have that Labs
18. 18.▲
    by henryrobbins00 3mo ago

    What a coincidence! I just released OpenATP earlier today. OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It includes support for Leanstral with Mistral’s Vibe harness. The previous production Leanst
19. 19.▲
    Show HN: OpenATP: A platform for automated theorem proving in Lean(github.com)

    3 points by henryrobbins00 3mo ago|0 comments
20. 20.▲
    Show HN: A website to track live music attendance(showcount.com)

    3 points by henryrobbins00 5mo ago|1 comments