FEfennecs·May 26, 2022Submission
Holbert: An Interactive Theorem Prover
68 points · Open discussionliamoc
holbert
Haskell2021–2022
liamoc / holbert
holbert
A graphical interactive proof assistant designed for education
2Distinct people
2Mentions
0Explicit recommenders
172GitHub stars
What to know before exploring
What it is
A graphical interactive proof assistant designed for education
GitHub
Where it is used
No documented product use has been verified yet.
What people are saying
No recommendation phrase was found in the indexed comments.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
No other repository is repeatedly linked in the same discussions.
This week on Hacker News
Nov 7–Nov 14 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/14/2026, 1:49:46 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by month2 dated mentions
Observed mentions: 2021-02-22 16:49:59 UTC to 2022-05-26 05:50:13 UTC.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| Feb 2021 | 2021-02-01 00:00:00 UTC | 2021-03-01 00:00:00 UTC | 1 | 0 | 1 |
| Mar 2021 | 2021-03-01 00:00:00 UTC | 2021-04-01 00:00:00 UTC | 0 | 0 | 0 |
| Apr 2021 | 2021-04-01 00:00:00 UTC | 2021-05-01 00:00:00 UTC | 0 | 0 | 0 |
| May 2021 | 2021-05-01 00:00:00 UTC | 2021-06-01 00:00:00 UTC | 0 | 0 | 0 |
| Jun 2021 | 2021-06-01 00:00:00 UTC | 2021-07-01 00:00:00 UTC | 0 | 0 | 0 |
| Jul 2021 | 2021-07-01 00:00:00 UTC | 2021-08-01 00:00:00 UTC | 0 | 0 | 0 |
| Aug 2021 | 2021-08-01 00:00:00 UTC | 2021-09-01 00:00:00 UTC | 0 | 0 | 0 |
| Sep 2021 | 2021-09-01 00:00:00 UTC | 2021-10-01 00:00:00 UTC | 0 | 0 | 0 |
| Oct 2021 | 2021-10-01 00:00:00 UTC | 2021-11-01 00:00:00 UTC | 0 | 0 | 0 |
| Nov 2021 | 2021-11-01 00:00:00 UTC | 2021-12-01 00:00:00 UTC | 0 | 0 | 0 |
| Dec 2021 | 2021-12-01 00:00:00 UTC | 2022-01-01 00:00:00 UTC | 0 | 0 | 0 |
| Jan 2022 | 2022-01-01 00:00:00 UTC | 2022-02-01 00:00:00 UTC | 0 | 0 | 0 |
| Feb 2022 | 2022-02-01 00:00:00 UTC | 2022-03-01 00:00:00 UTC | 0 | 0 | 0 |
| Mar 2022 | 2022-03-01 00:00:00 UTC | 2022-04-01 00:00:00 UTC | 0 | 0 | 0 |
| Apr 2022 | 2022-04-01 00:00:00 UTC | 2022-05-01 00:00:00 UTC | 0 | 0 | 0 |
| May 2022 | 2022-05-01 00:00:00 UTC | 2022-06-01 00:00:00 UTC | 1 | 1 | 0 |
What Hacker News says
2 sources> Both tactics and proof terms are already quite old (for CS concepts, that is) and there hasn't been any real competition, so I imagine in the medium-term we'll just see refinements of them.
So it's really more of an issue of presentation? The techniques are fine? (I'm a professional programmer but an amateur logician, I really don't know what the big kids do.)
> I can't imagine anyone wanting to read latex source code over tactics/proof term code. Unless you're talking about rendered latex?
Yeah, you would generally only be looking at LaTeX source to debug your tools.
> But that's not something people can realistically work with.
I don't understand. I rarely work with it, but I was under the impression that it's pretty standard for writing math and science papers? Are there no WYSIWYG tools for working with rendered LaTeX? How do p
Read the rest
eople work with it now, I guess is what I'm asking.
> Graphical proof assistants exist, but nobody uses them.
I just did a quick search and found two but they seem obscure:
https://en.wikipedia.org/wiki/Jape_(software)
https://github.com/liamoc/holbert
I guess the question I have is why does no one use them? Is it just inertia? I mean this is a thread about promoting the use of Lean et. al., so even the non-graphical, well-known tools are still kind of a niche, no?
Are graphical proof assistants only good for students and teaching, not "heavy lifting"?
In any event, I still feel that we can do better on the presentation side of things. (That's not controversial is it? The Lean folks are working on it?) I want to understand what kinds of software would help mathematicians.
> In a sense, tactics are a very weak form of this. Instead of just describing a proof as its structured in the system, they allow a proof author to also describe some of their intent or intuition. It's definitely why some people prefer tactics-based proofs.
That's pretty cool. :)
> I can't even imagine would formalizing something so subjective would even look beyond this. I'm not sure if it's even possible.
The Turing Machine is itself a formalization of a subjective process, eh?
If we get to the point where the machines can "read our minds" then it will be really easy. :) Heck, mathematicians can just watch videos of each other's mental imagery!
In the meantime, externalizing and formalizing these subjective intuitive processes with the machinery we've got seems like a fun and useful challenge, eh?