Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4
Leni Aniva, Claire Wang
Music theory obeys a rich set of mathematical rules and symmetries. These symmetries follow mathematical structures which can be verified and expressed in the precise language of a…
cs.LO2026
Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4
Leni Aniva, Iori Oikawa, David Dill +1
In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a statement in a proof assistant. In this work, we in…
cs.LO2024
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
Leni Aniva, Chuyue Sun, Brando Miranda +2
Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a sur…