3 ms·
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 usin
by Paracompact 28d ago
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.
- dnautics 28d agoWIP, but that is the target ethos in the prover I'm building: https://github.com/ityonemo/bpa 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
- IngoBlechschmid 27d agoI 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 https://github.com/martinescardo/TypeTopology