mathematical software developers

Abstract: Call a finite nonempty point set $S\subset\mathbb{R}^d$ all-even if for every direction $\ell \in \mathbb{P}(\mathbb{R}^d)$, the number of hyperplanes perpendicular to $\ell$ that intersect $S$ is even. In 2026, Francisco Santos presented a question of Juan Benigno Seoane-Sepúlveda on the existence of all-even sets in dimensions $3$ and higher, together with examples of such sets in dimension $2$. Call a set $S\in\mathbb{R}^d$ line-all-even if for every direction $\ell \in \mathbb{P}(\mathbb{R}^d)$ the number of lines parallel to $\ell$ that intersect $S$ is even. As Santos pointed out, every all-even set in $\mathbb{R}^3$ is line-all-even. We conjecture that there exist no line-all-even sets in $\mathbb{R}^3$ that affinely span $\mathbb{R}^3$ We show that our conjecture is equivalent to the statement that every planar all-even set satisfies a certain property, which we call height-rigidity. This property has a natural interpretation in linear algebra terms. Furthermore, we present a hierarchy of properties of planar point sets that imply height-rigidity. We construct several all-even sets in the plane, including some infinite families, and show that all the sets we constructed are height-rigid. In addition, we prove that every all-even set in the plane that can be covered by six or fewer parallel lines is height-rigid.

Abstract: Every semi-magic square of order $n$ satisfies the axial moment identities $\sum_{i,j}s_{ij}j^m=\sum_{i,j}s_{ij}i^m=M(n)\sum_jj^m$ for all $m\ge1$, where $M(n)=n(n^2+1)/2$. For real matrices the converse requires $1\le m\le n-1$, whereas for arrangements of $\{1,\dots,n^2\}$ fewer moments suffice once $n\ge14$. We define the permutation threshold $k^*(n)$ as the least $k$ such that every arrangement satisfying these identities for $1\le m\le k$ is semi-magic. In terms of the column-sum deviations $γ_j$, the degree-$k$ conditions state that $\sum_jγ_jt^j$ is divisible by $(t-1)^{k+1}$, linking $k^*(n)$ to the Prouhet--Tarry--Escott problem. While Schur's bound on real zeros gives $k^*(n)\le\sqrt{2(n-1)\log(n^4/4)}$, we prove the converse realisability bound $k^*(n)\ge(\sqrt2-o(1))\sqrt n$ (and $k^*(n)\ge(\sqrt6-o(1))\sqrt n$ when $4\mid n$) by perturbing semi-magic squares with complementary row pairs via horizontal swaps. We also show that $k^*(n)=n-1$ for $3\le n\le13$, $k^*(n)=n-2$ for $14\le n\le17$, and $k^*(n)\le n-3$ for $n\ge18$, and determine $k^*(n)$ for $18\le n\le40$ with computer assistance. Finally, at the $k=1$ level of the hierarchy, we specialise the Mantel--Hubert quadratic assignment variance formula to obtain exact means, variances, and limit laws under a uniform random arrangement for the full line-sum energy $E_{\mathrm{full}}$, for the four-term energy $E_4$ combining the first moments and the two diagonals, and for Loly's moment of inertia, and find that $|L_4|=14{,}639{,}440$ arrangements of order $4$ satisfy $E_4=0$.

Abstract: The diagonals of a regular pentagon dissect it into eleven pieces and draw a pentagram; the dodecahedron dissected by the twelve face planes of its inner core gives Kramer's seven "elementary cells" of 1982. We define the stellation dissection of a golden regular polytope in any dimension as the dissection of the convex hull of its final regular stellation by the facet hyperplanes of the core, show that the core has phi^(-d) of the inradius of the hull for d = 2, 3, 4, and carry the dissection out for the first time on the 120-cell. The foundation is the arithmetic of the golden ring Z[phi], the ring of integers of Q(sqrt 5): vertices and hyperplanes live in Z[phi]^d, every orientation test is the exact sign of an element of Z[phi], decided with integers, and the pieces are named by sign vectors. We develop this foundation from scratch (conjugation, norm, units, the primes sqrt 5, 2, 3, the exact sign test, the lattice x -> (x, conj x), the vertex modules of the dodecahedron and the 120-cell, the icosian ring) and let it carry the geometry. The definition bifurcates in dimension four: the star cut at depth phi^(-4), a unit, has 2,455,201 cells in 338 orbits of H4; the hereditary cut at depth 1 - phi^(-4) = sqrt 5 / phi^2, a unit times the ramified prime, induces the three-dimensional dissection on every facet and has 8,161 cells in 8 orbits. New here: all vertices of the dodecahedral and of the hereditary dissection lie in the vertex module of the polytope being cut, whereas the star cut needs the denominators 2, 3 and 5; the seven kinds of pieces of the dodecahedron are exactly the I_h-orbits of sign vectors, with stellation layer equal to the number of plus signs. We catalogue the four-dimensional pieces and treat the circumscribed disc, ball and 4-ball. Every number quoted is recomputed exactly by a script whose output is reproduced in an appendix.

Abstract: While artificial intelligence has made rapid progress in mathematical reasoning, many open problems depend on structure that is revealed only through large-scale computational exploration and analytical synthesis. One such example is Lehmer's problem from 1933. It asks whether the Mahler measure of an integer polynomial, which measures how far its roots stray from the unit circle, can be made arbitrarily small. Previously, constructing irreducible polynomials with integer coefficients and small Mahler measure has been carried out systematically only for even degrees $d \le 180$. At higher degrees, Boyd's analytical one-parameter family frequently factors, skipping nearly 50% of target degrees and leaving no general construction for arbitrary $d$. Here, we address the high-degree regime through a human-AI discovery loop, in which we extend the conversational prompting with a fast numerical pipeline, an exact symbolic verifier, and large-scale distributed search. The AI agent prototypes numerical and symbolic solvers locally, launches parallel searches across distributed clusters and works with the human researcher to extract and verify mathematical hypotheses. Through this interactive loop, we derive a five-parameter construction, which we call the Generalized Boyd algorithm. It eliminates degree-skipping and constructs irreducible polynomials with Mahler measure strictly below Boyd's limit point $α_1 \approx 1.255434$ for every target degree. Evaluated across all even degrees up to 2000, our approach improves upon six previously published values and holds 99.6% of all best known records. With this work we release the verified dataset of polynomials with minimal Mahler measure across all studied even degrees.

Abstract: Coherent differentiation has been introduced a few years ago as a refinement of the (categorical semantics of the) differential lambda-calculus and of differential linear logic, compatible with the determinism of computation, and hence in categories where addition of morphisms in the hom-sets is only partially defined. In this setting differentiation is implemented by a kind of ''tangent functor'', with the difference that it maps an object to its object of summable tuples rather to a tangent bundle. In our earlier work, these tuples were pairs in the case of simple differentiation, and families indexed by integers when dealing with Taylor expansion and the Fa{à} di Bruno formula. We push this idea further, considering now tuples indexed by an arbitrary commutative partial monoid satisfying a nonnegativity condition. The monoid structure on these indices plays a crucial role in the definition of the ''differential'' calculus associated with this ''tangent functor''. In that way, and without changing the general categorical infrastructure of coherent differentiation, this theory accommodates new notions of ''differentiation'' of which we describe several instances. Among many others, such notions include various forms of finite differences as well as Taylor expansion truncated at any fixed degree, and finite Taylor expansion of a fixed finite degree with a remainder.

Abstract: Part I [arXiv:2606.30202] and Part II establish which trust-region radius update mechanisms can fail and under which hypotheses they must succeed. Neither says where the thresholds sit once a rule runs with real constants, or how the rule interacts with the model Hessian and the subproblem solver. This paper turns them into nine falsifiable claims and settles what it can, on four designed problems where the theory's quantities are computable and on CUTEst, where only aggregate cost is visible. Every mechanism runs in one Julia package written for this study, so two runs differing in one component differ in nothing else. The rule is worth less than the model and more than nothing. Crossing the mechanisms with four model Hessians puts $96.5$ per cent of the variation on the model and $1.6$ on the rule, and the rules separate most under the most accurate model rather than least. Uncapped R-grad is the robust default among the criticality-anchored rules, though the retrospective rule is ahead of it on this collection. No constant escapes the side conditions. For every cap there is a minimiser at which the constraint stays active, and for every anchoring constant a flatness on which escape takes arbitrarily long. The second of these is proved here as well as measured, and the proof uses no property of the model or of the subproblem solution beyond $\|s_k\| \leq Δ_k$. The radius rule governs the length of the step, and so the cost of a run. The model decides the search direction, and with it whether the run converges at all.

Abstract: We demonstrate an application of deep learning to the problem of identifying whether two generating vectors correspond to topologically equivalent finite group actions on Riemann surfaces, showing how architectures developed for semantic understanding have use for pure mathematical problems. In doing so we discuss how desired algebraic structure influences model design, and explore which structural properties of topological equivalence classes the model has successfully learnt.

Abstract: The completion problem for continuous and Archimedean triangular norms (t-norms for short) consists in describing all the operators that take predefined values on a given subset of the unit square, and it reveals how much of a t-norm is determined by partial information. In this paper, we focus on the case where this subset is a parametric curve. We first formulate the problem in terms of the functional equation satisfied by an additive generator, and we then restrict our attention to curves of the form $(x,p(x))$ with $p$ continuous and increasing, which include the classical diagonal and horizontal section cases. We determine when the known values are compatible with a continuous and Archimedean t-norm, and we show that every completion is obtained by choosing the additive generator on a subinterval and reconstructing it elsewhere from the values on the curve. This description is recursive in general and becomes a closed formula under additional conditions, recovering the two classical results as particular cases. The completions are not unique, and we give examples with infinitely many t-norms sharing the same section along a curve. Finally, we combine our results with the reconstruction of a t-norm from its values above a level curve, which determines exactly the additive generator on that subinterval, so that the two pieces of information are complementary and together determine a unique completion.

Abstract: We prove the weak composition-independence conjectures of Kohn, Marchetti, Massarenti and Mella. The proof uses deformations of rational curves and a single kernel of the linearized equation. Riemann-Roch gives a contradiction from tangent fields with controlled poles. By settling these conjectures, we prove that a neural network with a general polynomial activation function of sufficiently large degree is identifiable.

Abstract: Recent progress in autoformalisation of mathematics using AI has been impressive. Measuring this progress requires datasets of formal statements that are both hard and trustworthy. We present AnnalsChallenge: 50 formalised theorem statements written by hand in Lean 4 using Mathlib. Each is the main result of a paper published in the Annals of Mathematics since 2020. Every formalisation was manually reviewed and then audited by AI. We release them without formalised proofs.

Abstract: Euler's constant $γ$, also known as the Euler-Mascheroni constant, remains one of the most elusive constants in mathematics. Despite extensive study, its irrationality is still unproven, and Apéry-like approximations of it are remarkably scarce. We present a novel identity that expresses $γ$ in terms of a Meijer G-function and its first few derivatives. This identity is then generalized and used to systematically generate infinitely many Apéry-like approximations of $γ$ using a Conservative Matrix Field construction based on the Meijer G-function.

Abstract: Links are disjoint unions of circles smoothly embedded in $S^3$. We use reinforcement learning and Bayesian optimisation to obtain new upper bounds on several link invariants that are not known to be algorithmically computable: the slice genus and the unknotting number for links, and the strong slice genus for algebraically split links. We also compute lower bounds using known invariants. Combining the upper and lower bounds, we obtain new exact values in many cases. Our unknotting agents can reproduce the non-additivity of the unknotting number for several counterexamples due to Brittenham and Hermiller, in some cases finding new unknotting trajectories.

Abstract: Large language models are increasingly contributing to mathematical research, where progress often depends on efficient proof search, incremental improvements and careful verification. We describe Bolzano, a multi-agent open-source system that uses parallel prover agents with a verifier agent and maintains a human-readable research state. Initial manual use on expert-selected problems yielded 8 results whose proofs were checked by domain experts. Motivated by these case studies, we ran Bolzano without problem-specific human guidance on about 3,800 open problems extracted from four sets of papers, solving about 200 open problems. One experiment used papers accepted to STOC 2026, a top conference in theoretical computer science. There, we answered four questions raised in the papers, as confirmed by their authors.

Abstract: Let N(T) count the nontrivial zeros of the Riemann zeta function up to height T with multiplicity, N_d(T) the distinct ones, and N_0^s(T) those that are simple and on the critical line. We prove liminf N_d(T)/N(T) >= 1645064/1960733 = 0.83900...; earlier work proves 0.83699..., and a report we have not verified claims 0.83805.... Hence more than 67.80% are simple. Also liminf N_0^s(T)/N(T) >= 0.67353...; earlier work proves 0.67250..., and reports we have not verified claim 0.673492. Two estimates of Lamzouri are improved: at least 88.93% of the zeros are simple or on the critical line, and the proportions of simple zeros and of zeros on the line average at least 83.67%. By the unconditional form of Montgomery's pair-correlation theorem the energy, a sum of a test function over pairs of zeros, is known asymptotically. A zero of multiplicity d contributes d^2 to it and nearby zeros contribute too, so a lower bound for such pairs leaves less energy for multiple zeros. The proof has three steps. First, for zeros at least a fixed fraction of the mean spacing apart, a large sieve inequality lets their pairs be used in full, with multiplicities. Second, their contribution is bounded below by a computer-assisted inequality for seven or eight consecutive zeros which distinguishes simple and double zeros. Its correction terms telescope, as increments of a storage function. Third, the test function is chosen to make this contribution large, at the cost of more energy. We also prove upper limits for what such inequalities can give with the two main test functions. The lower bounds and these limits are proved in Lean 4, analytic inputs included. The proofs use three axioms beyond those of Mathlib, one per inequality. Each records that a search program returned true; Lean's kernel does not check the run itself. This work is an experiment in AI-assisted mathematical research.

Abstract: This article offers an introduction to metaprogramming in Isabelle/HOL for beginners, based on a running example for working with multivariate polynomials. The example is motivated by our formalisation of universal Diophantine pairs. We describe the implementation of the poly_degree command, which computes upper bounds on the total degrees of multivariate polynomials and automatically proves their correctness. The complete metaprogram handles a variety of special cases but herein we present a simplified version for the sake of exposition. We describe our development process and design decisions; our goal is to offer a small and self-contained tutorial on Isabelle/ML, for mathematicians who want to get started with metaprogramming.

Abstract: Supersingular abelian surfaces are essential in isogeny-based cryptography. Despite this, we have no efficient algorithm to verify if a given abelian surface is supersingular. In this work, we initiate this research topic by giving an efficient Monte Carlo algorithm to verify if an abelian surface over $\mathbb{F}_p$ is supersingular in $O(\log p)$ with negligible failure probability, and an efficient conclusive algorithm if the order is smooth. We derive this algorithm by a careful analysis on the structure of supersingular Jacobians over $\mathbb{F}_p$. Furthermore, we derive efficient algorithms to verify if an abelian variety of any dimension is minimal or maximal, and to verify if a Jacobian of any dimension is superspecial.

Abstract: Skill evolution offers a promising way to improve large language model agents without updating their parameters, but its use in formal theorem proving remains underexplored. Existing methods mainly target natural-language reasoning, improving skills by analyzing successful and failed trajectories and incrementally revising solving strategies. Although the Lean verifier provides reliable execution feedback, when all sampled trajectories fail, existing skill evolution methods lack successful trajectories from which to infer effective update directions. Furthermore, these methods also focus mainly on the root instruction file, thus underexploring the evolution of reference knowledge including mathematical concepts and proving techniques. To address these limitations, we propose a mutation-enhanced skill self-evolution framework for building skill-augmented Lean provers. The framework jointly evolves a high-level solving policy and its reference knowledge through progressive and mutation-based updates. Progressive evolution derives local improvements from successful and failed trajectories, while mutation is triggered when no complete proof can be generated, sampling mathematical concepts to produce and select new skill candidates under verifier feedback. We evaluate our method on MiniF2F, PutnamBench, the 2025 International Mathematical Olympiad (IMO 2025), and the 2026 USA Mathematical Olympiad (USAMO 2026). Under the same backbone model, trajectorysampling budget, and test-time compute, our method achieves proof success rates of 100.0%, 90.6%, 4/6, and 4/6, respectively, with GPT-5.5, outperforming the baseline methods. Further analysis shows that concept-guided mutation outperforms random-text-guided mutation by 6.9 and 8.2 percentage points on MiniF2F and PutnamBench, respectively, while solving one additional problem on both IMO 2025 and USAMO 2026.

Abstract: Every scalar ordinary differential equation of order at least three with rational right-hand side that is locally linearizable by a point transformation admits a linear form with rational coefficients over the same coefficient field. We prove this by restricting the derived symmetry algebra to a coordinate line and recovering a scalar differential operator from rational symmetry-jet data. The construction uses differential elimination and linear algebra; it does not require the symmetry generators or a linearizing transformation to be solved for. A single integer parameter suffices to choose the line.

Abstract: Recent achievements in AI-assisted mathematics require intensive interaction of agents with proof assistants to generate machine-checked proof certificates. Agents interact with proof assistants such as Rocq or Lean through an interface that controls what the agent receives from the prover and the cost of these interactions. Today, these interfaces are adapted from tools designed for humans and not optimized for agents. We propose an evolutionary method where a frontier model incrementally proposes new features and only keeps the ones that improve the overall performance of smaller models. We demonstrate the effectiveness of our method by growing, on a curated set of mathematical problems, \rme, a new MCP server for the Rocq prover. On the held-out \texttt{test} split of miniF2F-Rocq, an agent equipped with \rme outperforms both the baseline that only exposes the Rocq compiler and an established MCP server, across four models from two families, in success rate, cost per solve, and time per solve. Although evolved for Rocq, the resulting server transfers to Lean, improving cost and time per solve on a subset of PutnamBench. We release \rme and its port to Lean.

Abstract: We present gap-lean4-port (Release v0.2.0), a machine-checked formalization of foundational algorithms in computational discrete algebra and permutation group theory within the Lean 4 interactive theorem prover and Mathlib4. While modern proof assistants feature extensive abstract algebraic hierarchies, constructive and operational permutation group algorithms, such as Charles Sims' 1970 Schreier-Sims algorithm, transversal tree lookups, and backtrack ordered partition refinement, have remained largely unformalized in dependent type theory. Here, we formalize the operational algorithmic core of the Groups, Algorithms, Programming (GAP) system library across four foundational modules, proving 35 machine-checked theorems with zero unproven conjectures (sorry) and zero custom axioms under standard Lean 4 foundations (propext, Classical.choice, Quot.sound). We machine-check: (1) Schreier-Sims stabilizer chain hierarchies (StabLevel, StabChain) and the invariance of incremental transversal tree extensions (extendSchreierPoint_invariant); (2) single-level and multi-level Schreier sifting reductions (siftOneLevel, siftFull), proving that full sifting strictly fixes all base points (siftFull_fixes_all_basePoints); (3) constructive soundness and completeness of Base and Strong Generating Set (BSGS) membership testing (membershipTestKnownBase_iff_mem); (4) backtrack ordered partition cell refinement (splitCellByPred), proving mutual cell disjointness, union conservation, and exact cardinality preservation; (5) cyclotomic extension rings Z/nZ(eps_m) and machine-check GAP's exact size theorem |Z/nZ(eps_m)| = n^m; and (6) executable Bezout inverses via Extended Euclidean GCD (Nat.gcdA) over residue rings Z/nZ. The entire codebase compiles deterministically under 'lake build RequestProject' and is openly available at https://github.com/pCwOrM/gap-lean4-port.

Abstract: We study generalized Blaschke curves as a controlled environment for AI-assisted mathematical rediscovery. For one fixed degree-four Blaschke product, an agent receives numerical coordinates of the six pair-lines determined by each of 80 boundary configurations. The target theorem is withheld from the task instructions. The saved research log reports rejected geometric hypotheses and a homogeneous cubic fitted to polygon sides. Its frozen coefficients predict 480 lines from 80 unseen parameter values, with a recorded RMS scale-free residual of $8.88\times10^{-17}$. Discovery-set diagonals provide an out-of-fit consistency check, not a fully held-out test. A separate one-configuration run reports insufficient evidence for invariance. A post-review deterministic degree-search baseline also recovers the cubic, so the experiment does not establish an advantage over polynomial fitting. We present this single-instance case study as a protocol for separating conjecture, numerical validation, and proof, with explicit limitations concerning agent metadata, prior knowledge, and reproducibility.

Abstract: We present GenLimitLib, a source-aligned Lean 4 library for language generation in the limit. Introduced by Kleinberg and Mullainathan at NeurIPS 2024, language generation in the limit studies a theoretical question motivated by LLMs: how to generate valid new strings from observed examples. This young and rapidly evolving field offers a natural testbed for studying large-scale formalization. GenLimitLib contains formal developments for 30 papers. It extracts shared definitions and reusable proof components while preserving paper-specific assumptions and statements, and records relationships across papers. In this way, GenLimitLib provides a concrete and structured view of the literature. We show through mathematical case studies and LLM experiments how our library can support both human mathematical research and AI-assisted research. Our Library: https://github.com/pengzhang91/generation-in-the-limit-lib.

Abstract: We introduce Solver Agent, an AI framework based on large language models for calculations and proofs in mathematics and theoretical physics. The solution process is tracked through a persistent ledger that records assumptions, derivations, and computations. A central agent delegates tasks to specialized sub-agents, while independent agents verify both intermediate steps and the final result. This setup improves the traceability, reproducibility, and verification of computer-assisted calculations. Applying Solver Agent, we study global F-theory uplifts of Type IIB orientifolds and their S-fold generalizations. We establish sufficient conditions for Weierstrass models over projective threefolds with terminal $\mathbb{Z}_k$ quotient singularities ($k\in\{2,3,4,6\}$) to give $\mathbb{Q}$-factorial projective elliptically fibered Calabi-Yau fourfolds with isolated Gorenstein terminal quotient singularities. These geometries realize O3-planes and S-folds, where local D3-brane probes of the latter yield four-dimensional $\mathcal{N}=3$ superconformal field theories. Using stringy invariants, we derive fixed-point contributions to Hodge data and Euler characteristics, and show that these Euler corrections determine the localized D3-brane charges required for tadpole cancellation. We illustrate these results using toric hypersurface constructions, where a single three-dimensional polytope determines both the Type IIB Calabi-Yau threefold and the F-theory base; here, the orientifold double cover naturally forms a bisection of an alternative genus-one-fibered uplift with discrete $\mathbb{Z}_2$ gauge symmetry. Finally, we provide methods for toric computations and four-form flux analysis in four-dimensional $\mathcal{N}=1$ compactifications with non-abelian gauge sectors.

Abstract: Does structured mathematical knowledge help LLMs prove theorems in Lean 4? If so, for which models, and does the answer vary by problem? Formal libraries such as Mathlib encode 285,000+ verified theorems with syntactic dependencies, but the semantic layer mathematicians rely on for discovery (analogies, generalizations, cross-domain bridges) remains implicit. We introduce MathAgent, which builds this layer as a knowledge graph, MathKG, and uses it to augment LLM theorem provers. MathKG connects 364 Mathlib theorems and definitions by 9,434 typed semantic edges inferred via LLM-based relation extraction anchored to verified Mathlib declarations. We run a controlled ablation across four augmentation modes (no context, knowledge-graph context, Mathlib retrieval, both) and five models: Qwen3-8B/32B, their Lean-specialized derivatives Goedel-Prover-V2-8B/32B, and Claude Sonnet 4.6, on miniF2F, plus PutnamBench and MathOlympiadBench for Sonnet. Three findings emerge. (i) Specialization dominates augmentation: Lean fine-tuning adds 33-38 percentage points of solve rate in every mode, and a specialized 8B model beats a $4\times$ larger general one by 29-35 points, while no augmentation mode improves solve rate by more than 3 points. (ii) Augmentation is capability-conditioned: knowledge-graph context helps small models but hurts large ones, with the specialized model gaining more relative to its general base at every scale. (iii) Yet the augmentation modes solve different problems: an oracle selecting the best mode per problem solves 6% to 58% more than the unaugmented prover, a complementarity effect that strengthens on harder problems (32% more on PutnamBench). These results motivate adaptive strategies that select augmentation by model capability and problem. Code, data, and artifacts are available at https://github.com/sarehnabi/mathagent

Abstract: Mathematical expressions and the numerical behavior they produce are two views of the same underlying function, and connecting them is central to scientific discovery. Symbolic Regression (SR) relies on this connection directly: it searches for an expression that reproduces a given behavior. Recent multi-modal models learn this connection by embedding symbolic expressions and their numerical behavior in a shared representation space. We show that this embedding space is only globally aligned: complete expressions correspond to complete behaviors, but the contribution of individual parts of an expression is not represented. This granularity gap leaves the model unable to tell how a local edit to an expression changes its behavior, the central operation in SR. We introduce a compositional alignment method that closes this gap: a structural positional encoding exposes the substructure of an expression to the encoder, and a multi-granularity contrastive objective grounds each subexpression in the behavior it produces before propagating this grounding to the full expression. The resulting representations close much of the modality gap between symbolic and numerical embeddings, reliably distinguish the effects of local edits that the original alignment cannot, and transfer to external SR corpora.

Abstract: We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, organization of the project, the blueprint, and the main design decisions behind the formalization. It is the result of a large collaborative effort, written and developed in public.

Abstract: Scientific data span heterogeneous structures, including coordinates, networks, surfaces, volumes and fields, yet their topology can be quantified within a common framework through graph connectivity, cycle structure, genus and spatial embedding. Graph- and homology-based summaries do not determine spatial embedding, while standard knot and link polynomials require extensions to accommodate branching graphs. Here, we introduce KnottedGraph, a computational framework that converts such scientific representations to knotted graphs that retain graph connectivity and spatial embedding together. It constructs projected diagrams and PD codes, enabling various topological analyses, including Yamada-polynomial evaluation for topological classification. For scalable exact evaluation, it combines partial resolutions that leave the same unresolved connections and optimizes their processing order; the resulting algorithm is verified against published topological invariants of knotted graphs with up to 500 crossings. This scalability enables us to introduce an LLM-assisted mathematical-discovery methodology, in which computational topological data generated across knotted-graph families are used to identify candidate closed-form formulas. With this approach, we identify analytical Yamada-polynomials for generic graph motif families exhibiting Abelian and non-Abelian word sequences. Together, these scalable capabilities make knotted-graph topology computationally accessible across scientific domains, enabling large-scale classification and introducing a route from topological data to LLM-assisted AI4Math discovery.

Abstract: We report an explicit construction of a 27 x 27 x 27 symmetric tensor with rational entries that has tensor rank 55 over the rational numbers and symmetric tensor rank 56 over the complex numbers, providing a small counterexample to Comon's conjecture over the rational, real, and complex numbers. The construction follows the framework of symmetric adjoins introduced by Shitov. The primary technical contribution of this work is to prove a special case of Conjecture 6 appearing in Shitov's seminal 2018 work.

Abstract: In symbolic dynamics, the fixed-point construction from arXiv:0910.2415 defines shift spaces of finite type whose configurations embed infinite hierarchies of tilings. This article provides a "black box" abstraction of this method phrased in terms of substitutions and $S$-adic limit spaces operating over sequences of increasingly large alphabets. By quantifying the amount of information computed by the substitutions at each level, and using a suitable parallel model of computation, we provide a simple positive criterion of multidimensional soficity that generalizes classical examples from the literature.

Abstract: We present a two-part neural framework for forced three-dimensional incompressible Navier--Stokes flow. Part~I develops the computational forcing system. A physics-informed neural model generates structured external-force trajectories, candidates are optimized through differentiable PDE rollouts or PPO-Clip, and selected forcings are frozen and checked by independent fixed-force replay. Part~II provides the mathematical certification layer. It separates neural candidate discovery from continuum analysis, derives integrated reciprocal-vorticity criteria that imply Riccati-type growth and finite-time loss of smooth continuation, develops a validated computational-to-continuum transfer strategy, and establishes a conditional positive-probability closure for a nondegenerate neural output law. The proof is complete at the continuum level.

Abstract: We prove that exact Euclidean SVP is NP-hard under deterministic polynomial-time many-one reductions for full-rank cyclic integer lattices, equivalently full-rank ideals of $R_N:=\mathbb{Z}[X]/(X^N-1)$ in the coefficient norm. Hardness holds with $N=q-1$ for a varying odd prime $q$. As an application, we prove the same hardness for the algebraic class of NTRU-form lattices $\{(x,z)\in R_N^2:Hx\equiv z\pmod{QR_N}\}$, where $H,Q$ are unrestricted inputs. The decision problems are NP-complete, and the exact search problems are NP-hard under polynomial-time Turing reductions. No hardness claim is made for cryptographic NTRU parameter subclasses or key-generation distributions.

Abstract: We construct a simple rank-$7$ oriented matroid on $24$ elements with no simplicial tope, disproving the Las Vergnas simplex conjecture from 1980. We then show that the mutation graph on uniform oriented matroids is disconnected for infinitely many values of rank $r$ and ground-set size $n$, disproving the Cordovil--Las Vergnas conjecture from 1988.

Abstract: Artificial intelligence threatens to outrun human understanding and control. New mathematics is needed to design AI that is legible, steerable, and cooperative with humanity. I organize this invitation by mathematical field, so you can turn straight to your own: logic and game theory for cooperation; probability for agency and world-models; algebra and representation theory for learned features; analysis and geometry for generalization and training dynamics. Each section ends with an open problem that is accessible to a working mathematician with no prior experience in AI safety.