29 citations · 74 across the 24 of their papers we have counts for
3 papers · 2 filters
Optimising Metamath Proofs for Human Working Memory
Jeremy Lindsay, Cezary Kaliszyk, Christine Rizkallah
Mathematical proofs vary in legibility. While most proof optimisation techniques seek to minimise proof size, the strategic reordering of inferences can reduce the working memory d…
Polymorphism Meets DHOL
Rhea Ranalter, Florian Rabe, Cezary Kaliszyk
DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-b…
Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
Chad E. Brown, Cezary Kaliszyk, Josef Urban
We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multip…