Hacker News: henryrobbins00

New comment by henryrobbins00 in "Leanstral 1.5: Proof abundance for all"

henryrobbins00 — Sat, 04 Jul 2026 01:42:04 +0000

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 Code + Codex still out-perform Leanstral). My genuine aim is to share that usefulness with others, not self promote!

New comment by henryrobbins00 in "Leanstral 1.5: Proof abundance for all"

henryrobbins00 — Sat, 04 Jul 2026 00:38:43 +0000

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: https://github.com/henryrobbins/open-atp

Docs: https://open-atp.henryrobbins.com

New comment by henryrobbins00 in "Leanstral 1.5"

henryrobbins00 — Wed, 01 Jul 2026 11:46:15 +0000

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 setting enabled? When I contacted support, they said "enabling Labs models isn't available for self-serve activation on standard individual accounts." Do you have a different type of account?

New comment by henryrobbins00 in "Leanstral 1.5"

henryrobbins00 — Wed, 01 Jul 2026 03:30:25 +0000

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 Leanstral model was deprecated on May 22nd. I will update the package to point to Leanstral 1.5 ASAP!

GitHub: https://github.com/henryrobbins/open-atp

Docs: https://open-atp.henryrobbins.com

Show HN: OpenATP: A platform for automated theorem proving in Lean

henryrobbins00 — Tue, 30 Jun 2026 12:53:10 +0000

TL;DR: I created a Python package to make running agentic automated theorem provers (e.g., Aristotle, Numina-Lean-Agent, Claude Code, etc...) as simple as

open-atp prove Lemma.lean result/ claude

I took a class on formal verification back in 2022 when I was an undergraduate. There was something incredibly satisfying about constructing proofs in Coq and knowing my statements were now formally verified. However, formal methods were so time consuming that they weren't practical in most industry settings. The rise of AI has changed that story: https://blog.janestreet.com/formal-methods-at-jane-street-in....

AI is producing algorithms and mathematical proofs far faster than humans can review them and formal methods offer a solution. Automated theorem provers take a statement formalized in a proof assistant like Lean and attempt to supply a proof. Unlike natural language proofs, these proofs can be machine-checked, reducing the burden of review on humans.

AI agents are powerful automated theorem provers. Even general purpose coding agents, like Claude Code, can be effective provers with the right skills and tooling. However, these methods are currently challenging to run. They require configuring Docker containers with the proper Lean environment and agent tooling (skills, plugins, MCP, credentials). Furthermore, there is not a common interface to existing provers.

OpenATP aims to solve both of these challenges! It makes it easy to run methods locally in Docker or remotely in Modal. It currently supports the following provers: https://open-atp.henryrobbins.com/en/latest/provers/index.ht....

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

Points: 3

# Comments: 0

Show HN: A website to track live music attendance

henryrobbins00 — Wed, 08 Apr 2026 20:42:40 +0000

TL;DR: I built a website that allows users to track the concerts they've been to. If you have strong opinions about engineering/design or how shows should be tracked (festivals, venues, etc...), I'd love to get your input!

For the past ~5 years, I've been tracking the shows I attend on my personal website (https://love-music-will-travel.henryrobbins.com). It's fun to see things like distance traveled and how many times I've been to certain venues. I know many friends who also track their shows through notes, ticket stubs, Excel, etc... It always bummed me out that I couldn't pore through their concert data myself...

showcount.com is my solution to that desire. It's essentially a public version of my old personal website, where anyone can make an account and manage a show list (mine is https://www.showcount.com/user/love-music-will-travel).

I'm currently on the lookout for other live music lovers and/or data nerds to try out the site and give opinions on various design choices. If any of the following topics are of interest to you, please reach out!

- How should venue name/location changes be handled? - How should music festivals be handled? - I have an initial version of an AI parser for loading in existing show lists; how can this be made more robust? - What else should have first-class tracking support (e.g., friends in attendance)?

As an aside, this project is also my first experiment with full-on vibe-coding / harness-engineering. I began the project with Cursor and then switched to Claude Code. I've been programming for the better part of a decade, mostly Python and Java. Full-stack development is relatively new to me. I include the tech stack below. Most decisions were made pragmatically based on what I thought would get me to a first version of the site as quickly as possible.

- Next.js web app hosted on Vercel - Fast API backend service (for the AI parsing) hosted on Railway - Supabase - Observability through Axiom (logging), PostHog (analytics), and Sentry (monitoring) - Clerk for user authentication - Google Maps API for venue locations - Claude API for the AI parser - Terraform for infra-as-code

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

Points: 3

# Comments: 1