A Survey of Weak Reasoning Assistants
summary
Argues that a practical middle ground between raw LaTeX and fully sound proof assistants exists and is useful, surveying concrete tools: a LaTeX linting approach that parses papers for common mistakes, Lamport-style structured proofs for stepwise justification, Penrose visual optimization for unsatisfiable constraints, QuickCheck-style property-based testing and SMT/Mizar-style pragmatic automation. Claims these tools trade formal soundness for ergonomics and liveness, reports existing prototypes and libraries working well enough to catch real errors and speed understanding even without full mechanization.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:10Meta: about the paper
- 1:21"Strong" Reasoning Assistants (SRAs)
- 6:07Hope: the situation for programs (vs. math)
- 9:56Structured Proofs and pf2: adding structure to BTEX
- 11:03Penrose³: adding structure to TikZ
- 12:00QuickChick: removing structure from Coq
- 13:40Suggested focus 2: less-sound proof assistant
- 16:08Questions for Discussion
related talks
27mProduction Language Specification - Requirements for Multiple Usages
29mDiagrammatic notations for interactive theorem proving
05m“Validating Lemmas with Rustdoc [...]”
36mWriting Valuable Papers
54mPanel: Mechanized Specifications for Real-World Programming Languages
19mTowards Mining Robust Coq Proof Patterns
20mUser Brainpower vs. AI Blind Spots in API Docs
29mLegalese: Software Eats Contract Drafting