philzook58/knuckledragger
View on GitHub ↗ ★ 181 Python
A Low Barrier Proof Assistant
6 mentions on Hacker News by 1 person: 0 stories, 6 comments · first 2024-12-24 · latest 2025-09-30
20082026
-
I'm working on Knuckledragger, a proof assistant shallowly based upon z3py https://github.com/philzook58/knuckledragger Yesterday I proved the infinitude of primes, which I was pretty happy with. https://www.philipzucker.com/knuckle_primes/…
comment by philzook · 2025-09-30 · in Ask HN: What are you working on? (September 2025) -
Love it! I was trying to use python as a dsl frontend to Z3 in a different way https://github.com/philzook58/knuckledragger/blob/ecac7a568a... (it probably has to be done syntactically rather than by overloading in order to make `if` `and`…
comment by philzook · 2025-06-14 · in Implementing Logic Programming -
…I wrote a small datalog from the Z3 AST to sqlite recently along these lines https://github.com/philzook58/knuckledragger/blob/main/kdrag...
comment by philzook · 2025-06-14 · in Implementing Logic Programming -
…to collect rules or interesting theories up in my python interactive theorem prover Knuckledragger https://github.com/philzook58/knuckledragger . Rewrite rule or equational theory looking things are easier to work with than things with…
comment by philzook · 2025-02-22 · in Where are all the rewrite rules? -
…the correspondence of Sheffer stroke to Boolean algebra in my python proof assistant knuckledragger https://github.com/philzook58/knuckledragger (an easier result than Wolfram's single axiom one). I was also intrigued reading about the…
comment by philzook · 2025-01-10 · in Who Can Understand the Proof? A Window on Formalized Mathematics -
…idea is to use more natural looking python as dsl for function definitions in my proof assistant https://github.com/philzook58/knuckledragger Also to see if I can make a nice-looking staged metaprogramming framework in python like buildit,…
comment by philzook · 2024-12-24 · in Symbolic Execution by Overloading __bool__