Papers for

mathematics software engineers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Deterministic methods identify key invariants in polynomial ideals

Deterministic Determination of Axial Constants, Sectional Regularities and Annihilator Numbers

Abstract: Axial constants and sectional regularities are recently introduced invariants of homogeneous polynomial ideals that, like the already earlier introduced annihilator numbers, depend on generic choices of coordinates. We provide effective characterisations of the genericity underlying these invariants in terms of $β$-maximal position and strong stability. In particular, we show that $β$-maximal position suffices for determining generic annihilator numbers and sectional regularities, while its combination with strong stability yields corresponding results for axial constants. We also develop deterministic linear algebra procedures for detecting the required generic positions and for computing these invariants.

Thu 15 OctSymbolic Computation
The gist
The paper deals with special mathematical properties of polynomial equations that change depending on how you look at them. The authors found clear ways to recognize the best conditions under which these properties behave consistently. They created step-by-step procedures using linear algebra—basically systematic calculations—to find these properties without relying on randomness. This helps ensure that the results hold deterministically and can be precisely computed.
Open → 2610.22251v1

Faithfulness evaluation for math statements needs context awareness

Aligning Faithfulness for Theory-Scale Autoformalization

Abstract: Autoformalization (AF) requires more than compilation: formal statements must preserve the meaning of their informal sources, a property known as faithfulness. An emerging frontier is the automated evaluation of this property, yet most existing methods operate at the statement level and produce whole-item verdicts, failing to reveal how individual expressions correspond or which contextual interpretations support the judgment. This omission is consequential because AF is inherently theory-scale: target statements derive their meaning from surrounding mathematical material and unstated conventions. We formulate faithfulness evaluation as a context-aware align-then-label problem: identifying phrase-level correspondences between informal and formal statements and assigning a faithfulness label to each under explicitly specified contextual interpretations and assumptions. We also introduce FaithAlign, the first theory-scale faithfulness benchmark comprising 460 items and 4,982 annotated phrase-level links, alongside FaithAlign-Gap, a companion set of 146 items with informal context and assumptions withheld. Each FaithAlign item includes the target statement pair, relevant context, formal dependencies, and, where needed, assumptions specifying one given interpretation. Across 8 models, GPT-6 Astra achieves the highest defect F1 at 47.8% and identifies all defects in only 4.5% of items with two or more defects. On FaithAlign-Gap, Astra identifies only 28.2% of undecidable items as such. These results show the difficulty of recovering context-dependent correspondences, establishing FaithAlign as a testbed for fine-grained, context-aware faithfulness evaluation.

Tue 13 OctComputation and LanguageArtificial Intelligence
The gist
When computers try to turn informal math descriptions into formal statements, it’s important that the formal version means the same thing as the informal one — this is called faithfulness. The authors explain that checking faithfulness is hard because math statements rely on context and assumptions around them. They built a detailed dataset and tested models on it, showing current AI struggles to accurately match informal and formal math at a fine level. Their work helps guide future improvements in making computers understand math precisely.
Open → 2610.18498v1

AI system solves open algebraic combinatorics problems and raises questions

AI Discovery in Combinatorics: From Problems to Solutions and Back to Bigger Problems

Abstract: We introduce $qt$Bench, a benchmark of 29 open problems in algebraic combinatorics. These problems ask for a simple combinatorial algorithm that explains given polynomial coefficients or identities. To help AI agents search for such algorithms, we provide a scaffold for playing with combinatorial objects, countering cheating attempts, and testing candidate solutions. To explore how far frontier AI systems can go on these problems, we collaborated with OpenAI, whose researchers obtained proposed solutions to several of them. This highlights bigger meta-problems: is AI discovery at scale ethical? How should these results be released? How should proof digestion be organized? We discuss these questions and give our views.

Mon 12 OctArtificial IntelligenceMachine Learning
The gist
Algebraic combinatorics involves finding simple rules that explain complex math formulas. The authors created a set of 29 challenging problems that ask for such simple rules. They worked with OpenAI to see how well AI could find solutions, and the AI managed to propose answers to several problems. This also led to bigger questions about how to share AI-made discoveries ethically and how to check if the proofs are correct.
Open → 2610.16555v1