Hacker News Reader

It warms my heart every time I see an interactive proof assistant being used to improve rather than simply slow down mathematical thinking.

After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.

View on HN

WIP, but that is the target ethos in the prover I'm building:

https://github.com/ityonemo/bpa

Its painfully verbose and explicit but its designed to let you cut down to the structure of the proof with a query language

I agree! Martín Escardó never tires to say that he uses the Agda proof assistant in exactly this sense, as a kind of interactive blackboard for taking notes and structuring his thoughts. The vast TypeTopology repository is the result of years of following this philosophy: https://github.com/martinescardo/TypeTopology

Reply on news.ycombinator.com