Tag: Rocq

• "Why not just use Lean?" (23 Apr 2026)
  
• Broken proofs and broken provers (15 Jan 2026)
  
• 50 years of proof assistants (05 Dec 2025)
  
• Memories: Edinburgh LCF, Cambridge LCF, HOL88 (28 Sep 2022)
  
• Porting libraries of mathematics between proof assistants (14 Sep 2022)
  
• Axiomatic type classes: some history, some examples (02 Mar 2022)
  
• ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician (08 Dec 2021)