4 papers
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…
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…
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…
Regularization and Reparameterization Avoid Vanishing Gradients in Sigmoid-Type Networks
Leni Ven, Johannes Lederer
Deep learning requires several design choices, such as the nodes' activation functions and the widths, types, and arrangements of the layers. One consideration when making these ch…