Calle Sönne | arXiv Science

arXiv2026

An Exotic Congruence for Irregular Weight Picard Modular Forms

We construct a new type of congruence from irregular weight mod $p$ Picard modular forms (for $p$ inert) to ones of regular weight, analogous to the one obtained by Kansal--Levin--Savitt in the Hilbert setting. The congruence is obtained by using a geometric Jacquet--Langlands phenomenon, as first established by Vollaard, to transfer irregular weight mod $p$ Picard modular forms from the Picard modular surface to a Shimura set. We call this an exotic congruence, since it relates mod $p$ automorphic forms associated to different groups. This congruence will be used in upcoming work of the author proving mod $p$ local-global compatibility for irregular weight Picard modular forms (in the $p$ inert case).

math.NT↗

arXiv2026

Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics

As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this, we present Formal Conjectures, an evolving benchmark of currently 2615 mathematical problem statements formalized in Lean 4. Sourced from areas of active mathematical research, the dataset features 1029 open research conjectures providing a zero-contamination benchmark for mathematical proof discovery, and 836 solved problems for proof autoformalization. Notably, the repository provides a structured interface connecting mathematicians who formalize and clarify problems with the AI systems and humans attempting to solve them. Demonstrating its immediate utility, the benchmark has already been leveraged to make new mathematical discoveries, including the resolution of open research conjectures. We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community. In this framework, AI-generated proofs and disproofs serve as a valuable auditing mechanism to iteratively improve the fidelity of the benchmark. Finally, we provide a standardized evaluation setup and report baseline results on frozen evaluation subsets, demonstrating a climbable signal that measures the current frontier of automated reasoning on research-level mathematics.

cs.AI↗