Hacker GitHub

← All repos

John-Nagle/nqthm

View on GitHub ↗ ★ 61 Common Lisp

nqthm - the original Boyer-Moore theorem prover, from 1992

20 mentions on Hacker News by 2 people: 1 story, 19 comments · first 2016-08-07 · latest 2026-10-14

Mentions per year 20 mentions · busiest year 2017 (5)
20082026
AllStoriesComments NewestTopOldest
  1. …to array theory. It took 45 minutes on the VAX 11/780 I was using back in the early 1980s.) [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2026-10-14 · in The Four Colour Theorem: The first time machines mogged mathematicians
  2. …[2] https://www.animats.com/papers/verifier/verifiermanual.pdf [3] https://github.com/John-Nagle/nqthm
    comment by Animats · 2026-08-16 · in The Case Against Formal Verification, 50 Years Later
  3. …permutations of one another”)." - Boyer and Moore [1] https://www.cs.utexas.edu/~boyer/acl.pdf [2] https://github.com/John-Nagle/nqthm/tree/master
    comment by Animats · 2025-06-14 · in Peano arithmetic is enough, because Peano arithmetic encodes computation
  4. …yet. I should have built up constructive set theory first, but I didn't realize that back then. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp... [3]…
    comment by Animats · 2024-12-17 · in Natural Number Game: build the basic theory of the natural numbers from scratch
  5. …system. LISP is a blast from the path. It's fun for retro reasons, but things have moved on. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/tree/master/src/CPC4
    comment by Animats · 2024-02-14 · in Why is Common Lisp not the most popular programming language?
  6. …It took about 45 minutes in 1981.) [1] https://sites.math.rutgers.edu/~zeilberg/Opinion160.html [2] https://github.com/John-Nagle/nqthm [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2024-01-19 · in Opinions of Doron Zeilberger
  7. …which implies much case analysis. Mathematicians hate case analysis. Computers are good at it. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2023-06-30 · in Will Computers Redefine the Roots of Math?
  8. …[3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp... [4] https://github.com/John-Nagle/nqthm
    comment by Animats · 2022-05-30 · in Grothendieck's Approach to Equality [pdf]
  9. …[1]. It's several thousand times faster on current hardware than it was on the DECSYSTEM 2060.) [1] https://github.com/John-Nagle/nqthm
    comment by Animats · 2021-06-26 · in Ask HN: Best “I brought down production” story?
  10. …Still makes many mathematicians unhappy. [1] https://www.cs.utexas.edu/users/boyer/acl.pdf [2] https://github.com/John-Nagle/nqthm
    comment by Animats · 2020-01-08 · in What people get wrong about Bertrand Russell
  11. …Good times back then. But we were way ahead of our time. [1] https://github.com/John-Nagle/pasv [2] https://github.com/John-Nagle/nqthm [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2019-09-09 · in The Future of Mathematics? [pdf]
  12. …[2] https://docs.microsoft.com/en-us/windows-hardware/drivers/de... [3] https://github.com/John-Nagle/nqthm [4] https://github.com/John-Nagle/pasv
    comment by Animats · 2017-12-24 · in Formal Verification: The Gap Between Perfect Code and Reality
  13. …Constructive mathematics has a basic soundness you don't get from systems with too many axioms. [1] https://github.com/John-Nagle/nqthm
    comment by Animats · 2017-08-05 · in ACL2
  14. …now that computers can do this in a second, complaining that it's too complicated seems whiny. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2017-07-16 · in What makes maths beautiful?
  15. …it takes a few seconds.) [1] https://www.amazon.com/Computational-Logic-Robert-S-Boyer/dp... [2] https://github.com/John-Nagle/nqthm
    comment by Animats · 2017-07-08 · in Where Do Type Systems Come From?
  16. …the VAX days. It's neat to see it prove the basic theorems of number theory in about a second.) [1] https://github.com/John-Nagle/nqthm
    comment by Animats · 2017-06-18 · in Hey programmers, we need to talk (2013)
  17. …original around 1980. Now it can prove the basic theorems of number theory in a few seconds.) [1] https://github.com/John-Nagle/nqthm
    comment by Animats · 2016-12-29 · in C++17 – better than you might think
  18. …calculus on kids. It's not even clear that classical geometry proof approaches are that useful. [1] https://github.com/John-Nagle/nqthm
    comment by Animats · 2016-12-24 · in Do Teachers Need to Include the History of Mathematics in Their Teaching? (2003)
  19. …else involved was an academic. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf [2] https://github.com/John-Nagle/nqthm/tree/master/nqthm-1992
    comment by Animats · 2016-09-30 · in A Hoare Logic for Rust
  20. ▲ 2
    Nqthm – the original Boyer-Moore theorem prover, from 1992
    story by jaredsohn · 2016-08-07 · 0 comments