The Proof Machine (2016)

BenoitP 27 points 4 comments July 27, 2026
incredible.pm · View on Hacker News

Discussion Highlights (1 comments)

siraben

I've been working on an interactive click-and-prove prover that is backed by dependently typed terms.[0] The Proof Machine only goes up to some Simply-Typed Lambda Calculus terms, whereas I have the logic sufficiently powerful to support recursion and reasoning about programs and equality. [0] https://touchproof.siraben.dev/

Semantic search powered by Rivestack pgvector
15,062 stories · 140,779 chunks indexed