7 papers
QEDIA: Quantum Program Verification in Lean
Yuanjie, Ren, Zhicheng Zhang +4
Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classica…
Choir: An Open Protocol for Distributed Multi-Agent Autoformalization
Yidi Qi, Melanie Weber
AI agents can now formalize entire textbooks and major theorems in proof assistants such as Lean, but current efforts are typically centralized: a single team runs all agents and b…
Computer vision and converse theorems
Yang-Hui He, Kyu-Hwan Lee, Thomas Oliver +1
Random matrices provide a well-established statistical model for a range of arithmetic phenomena. In this paper, we investigate the extent to which one- and two-dimensional convolu…
Murmurations, Mestre--Nagao sums, and Convolutional Neural Networks for elliptic curves
Joanna Bieri, Edgar Costa, Alyson Deines +5
We apply one-dimensional convolutional neural networks to the Frobenius traces of elliptic curves over and evaluate and interpret their predictive capacity. In keeping…
MerLean: An Agentic Framework for Autoformalization in Quantum Computation
Yuanjie Ren, Jinzheng Li, Yidi Qi
We introduce MerLean, a fully automated agentic framework for autoformalization in quantum computation. MerLean extracts mathematical statements from \LaTeX{} source files, formali…
Machine learning the vanishing order of rational L-functions
Joanna Bieri, Giorgi Butbaia, Edgar Costa +6
In this paper, we study the vanishing order of rational -functions from a data scientific perspective. Each -function is represented in our data by finitely many Dirichlet co…
Learning Fricke signs from Maass form Coefficients
Joanna Bieri, Giorgi Butbaia, Edgar Costa +6
In this paper, we conduct a data-scientific investigation of Maass forms. We find that averaging the Fourier coefficients of Maass forms with the same Fricke sign reveals patterns…