Don’t Call Us, We’ll Call You
summary
A small prototype proof assistant implements two modes: auto-search-first where the tool runs an automated search and halts to ask for user feedback, and proof-interactive where the user pilots while the tool suggests instantiations and fills holes. It proves a Peano arithmetic commutativity/totality lemma after the user instantiates an induction hypothesis and supplies an existential witness; the prototype is a quick hacked language (not tied to Coq/Agda), works on the simple example, and exposes challenges in explaining failed search and configuring strategies.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:49Research inspiration and prototype
- 3:14User-tool interaction modes
- 5:05Proof in natural numbers theory
- 8:16Tool explains failed proof search
- 12:18User takes over proof construction
- 15:11Interactive mode as copilot
- 19:05Interaction modes and design recap
- 20:52Challenges in automated proof search
- 22:40Tool development and future plans
- 23:45Q&A
- 24:26Collaboration for design insights
- 25:31Infrastructure and related work
- 26:53Proof paths and user choices
- 27:33Recovering full proof
- 29:39Explicit vs implicit proof objects
- 31:47Conclusion and Q&A
related talks
18mDeveloping a Dependently Typed Language with Runtime Proof Search
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
19mAutomated Verification of Fundamental Algebraic Laws
01h 34mFormal Logic Undressed
26mMechanical Proofs in an Array-Combinator Language
33mHolbert: Reading, Writing, Proving and Learning in the Browser
36mBarliman: trying the halting problem backwards, blindfolded
16mUntangling Mechanized Proofs