Invited Talks

Contributed Talks

Reinforcement Learning for Theorem Proving

Alex Best
Harmonic, Palo Alto, USA

I'll discuss recent advances training language models to prove theorems at a very advanced level via reinforcement learning on formal languages. I will cover the progression of these systems from proving standalone statements, to building up whole new theories. I'll give a demo of the system we have been developing with these techniques, called Aristotle, and survey interesting use cases so far. Additionally I will discuss the potential ways that a mathematicians work will change when incorporating these tools.

Mathematical Methods in Perturbative Quantum Field Theory and the Analytic Integration of Feynman Integrals

Johannes Blümlein
Deutsches Elektronen-Synchrotron (DESY), Zeuthen, Germany

We present recent advances in the analytic calculation of single scale Feynman integrals in renormalizable quantum field theories. We consider complete physical processes at large-scale high energy colliders, such as the anomalous dimensions, massless and massive Wilson coefficients and the massive form factors to three-loop order in QCD. The fundamental methods to be used are difference and differential equations, which have first to be established by guessing methods. The corresponding equations are huge. In the case of first order factorizing equations iterative-integral solutions are obtained. We also present computer-algebraic methods to solve non first order factorizing differential equations.

Vibe Coding, Vibe Proving, Vibe Mathematics …?

Bruno Buchberger
Johannes Kepler University Linz, Austria

I discuss two recent research areas combining symbolic computation and machine learning:

  • learning algorithms for mathematical problems from training data
  • proving by generating proof ideas through large language models and checking the ideas with a proof checker.

The first area is concerned with replacing provenly correct algorithms for algebraic problems (as simple as integer addition or as complex as Gröbner bases construction or Cylindrical Algebraic Decomposition) with algorithms (for example, Neural Networks) that have been trained on large sets of input-output examples for the respective problem. Why should one do that – knowing that probably the trained algorithm may be incorrect for certain inputs? Well, this is practically interesting if the computation times of the trained algorithm are drastically better. This has been proved to be the case by recent work by H. Kera and others.

In the talk, I will discuss whether it is sufficient just to compare the computation times of a provenly correct algebraic algorithm and an algorithm trained by machine learning from examples. I argue that one also must take into account the computation time for checking the results generated by the trained algorithm. In the extreme case, this may be equally costly as the generation of the output by an algebraic algorithm. I will analyze this in particular in the case of the Gröbner bases problem, where we do not only have to prove that the result is a Gröbner bases but also that the ideal generated does not change. Both questions may need considerable effort. The second question may need the application of what is called “an extended Gröbner bases algorithm”.

The second area is concerned with building up large mathematical knowledge bases (definitions, theorems, algorithms) together with formally checked proofs. This area existed for a long time under the name “Mathematical Knowledge Management” (MKM). The practical impact of work in this area on the daily work of mathematicians or for generating mathematical archives , however, was relatively low. The reason was that proof-checking, as the only algorithmic tool in MKM, still left enormous work for the mathematicians who added knowledge to such mathematical knowledge bases. With the THEOREMA system (around 2000) I tried to improve the situation by coming up proof-generating algorithms. However, still much of the work – finding essential proof ideas – was left to the mathematicians. With the new approach (for which the Aristotle system is a prominent example) much of the creative work of finding proof ideas (and interesting definitions, lemmata, theorems, algorithms) is automated by just “looking to the literature for relevant text expressed in the usual semi-formal mathematical language” using kind of a specifically trained LLM and submit the results found to a proof checker. (In the case of Aristotle, this is LEAN). This step can be viewed as a kind of “vibe proving” (generalizing the recent “vibe coding” approach for programming) or even “vibe mathematics”.

In the talk, I will discuss whether, in this approach, it would make sense to replace a proof checker by a proof generator like THEOREMA.

[More...]

36 Years of AI and Math

Martin Charles Golumbic
University of Haifa, Israel

Research considered to be “artificial intelligence” constantly redefines itself. As the disciplines within AI have evolved and changed over many decades, mathematical methods have provided the solid foundation of these diverse areas. The range of topics appearing in the literature has been impressive.

To help bridge the gap between new applications of technology and foundational mathematical research, we explore research in a variety of disciplines, with a particular emphasis on the foundations of AI and mathematical methods. Artificial intelligence (AI) has contributed to mathematical discovery, by guiding conjecture generation, assisting in formalizing mathematics, and exploiting its power to identify patterns in data and refine relationships between properties.

There has always been a strong relationship between mathematics and artificial intelligence, including applications of each discipline in the other. Computational geometry is central to much of motion planning in robotics. Combinatorial optimization is a primary tool in search, and a main ingredient of machine problem solving. Mathematical logic is arguably the appropriate language for AI, and the theoretical underpinnings of intelligent systems. Automated reasoning systems have provided a further motivation for work on non-standard, non-monotonic logics and belief deduction. Mathematical probability is the foundation of dealing with uncertainty. The mathematical theory of games is the basis for AI game-playing and models of strategy and fairness.

The state of the art and current challenges provide a wealth of opportunities to advance research in the interactions between AI and mathematics through interdisciplinary collaboration. We present a selection of topics from recent symposia as an indication of this, along with some early history of interaction between Math and AI and its development over the years.

[More...]

Formalization and Automated Reasoning in the Age of LLMs

Cezary Kaliszyk
University of Melbourne, Australia

As LLMs become part of the formalization pipeline, the key question is no longer only how to automate proof, but how to organize collaboration between human guidance, automated reasoning, and machine learning. I will discuss what forms of automation are most useful to humans and to LLMs, the kinds of proofs they tend to generate and learn from, and the role of proof style in effective formal development. I will also cover readability: when are human-created formal proofs hard to understand, and how this changes for generative-model augmented formalization.

From π to QFT: Symbolic Discovery at Scale

Ido Kaminer
Technion - Israel Institute of Technology, Israel

For centuries, formulas for mathematical constants such as π and e appeared sporadically, discovered by figures like Newton, Euler, Gauss, and Ramanujan. Inspired by experimental physics, we established the Ramanujan Machine collaboration, a program of experimental mathematics that discovers formulas at scale, including new identities for π and for Riemann ζ values. This effort runs on a global volunteer network contributing CPU time, enabling the discovery of thousands of formulas—now surpassing the total found by humans over centuries.

In this talk, I will show how combining these symbolic mathematical capabilities with large language models yielded the first example of automated unification of mathematical knowledge, revealing deeper organizing structure among constants. I will then outline potential applications to areas outside of number theory: efficient computation of hypergeometric functions and broader families of D-finite functions, with implications for computing Feynman integrals.

As another application of massive symbolic computation, I will discuss our recent contribution to modern toolkits for automated effective field theory. As a proof of concept, I will present our massive automated scan for quantum completions of gravity, showing that one-loop contributions can reproduce the curvature of gravity from flat-space quantum field theory.

I will conclude with a broader perspective on AI4Physics vs. Physics4AI, with recent examples from my lab.

  1. G. Raayoni, et al., The Ramanujan Machine: Automatically Generated Conjectures on Fundamental Constants, Nature 590, 67–73 (2021)
  2. O. Razon, et al., Automated Search for Conjectures on Mathematical Constants using Analysis of Integer Sequences, ICML 202, 28809-28842 (2023)
  3. R. Elimelech, et al., Algorithm-assisted discovery of an intrinsic order among mathematical constants, PNAS 121, e2321440121 (2024)
  4. M. Shalyt†, U.Seligmann†, et al., Unsupervised Discovery of Formulas for Mathematical Constants, NeurIPS 37, 113156 (2024)
  5. Beit Halachmi and I. Kaminer, The Ramanujan Library - Automated Discovery on the Hypergraph of Integer Relations, ICLR (2025); arXiv:2412.12361
  6. T. Raz, et al., From Euler to AI: Unifying Formulas for Mathematical Constants, NeurIPS (2025); arXiv:2502.17533

[More...]

Computational Algebra with Transformers: What Deep Learning Adds to Computational Algebra

Hiroshi Kera
Chiba University, Japan

Computer algebra has advanced with computing. Computing enables experimenting with theories, algorithms, and heuristics of computer algebra, supporting their verification and the study of their limitations. This survey overviews recent applications of deep learning, particularly Transformer models, to arithmetic and symbolic computation, and presents a new axis that deep learning can add to computer algebra. While not always offering interpretable or guaranteed computation, the learning-based approach can extract patterns of computation through observation of instances at enormous scale; exploiting this may lead to faster algorithms and the discovery of new heuristics. In addition, generating training sets for deep learning models gives rise to new symbolic computation tasks. I will also briefly introduce the CALT library as a convenient entry point for interested audiences.

[More...]

Machine Learning in Symbolic Computation - A Skeptical Perspective

Michael Kohlhase
Friedrich-Alexander Universität Erlangen-Nürnberg, Germany

Driven by an enormous investments and industrial hype machine ML methods and particularly LLMs are making great progress in public/industrial/scientific awareness and practices. Every discipline asks (and has to ask) what can ML/LLMs do for me and how will science change with the new methods?

Generally, we have to come to terms with how to best combine/reconcile methods from subsymbolic AI (ML and LLMs) with symbolic methods in our respective areas. The former are data-driven and excel at global coverage, but have deficits in prediction and explainability whereas the latter are human-driven, precise, and explainable, but do not scale well.

In this talk I will try to survey the shape of symbolic/subsymbolic AI (keeping a distance to the "AI hype" to separate some of the myth from reality) so that we can assess combination opportunities and strategies. Finally I want to conjecture some of the effects of the "subsymbolic AI boom" for traditionally symbolic disciplines like formalized mathematics, symbolic computation, and tertiary STEM education.

[More...]

Differential Algebraic Machine Learning in Linear PDE Solution Spaces

Markus Lange-Hegermann
Technische Hochschule Ostwestfalen-Lippe, Germany

We consider linear constant-coefficient PDE systems. We present a computational differential-algebraic approach to probabilistic and learning-based models that work directly within their solution spaces. The starting point is the Ehrenpreis–Palamodov fundamental principle, which describes solutions through algebraically computable characteristic varieties and exponential-polynomial Fourier-type modes. We use this representation to construct two learning approaches within the solution spaces of such PDEs. First, it yields Ehrenpreis–Palamodov Gaussian processes: Bayesian priors concentrated on admissible PDE solutions, supporting conditioning on sparse, noisy, initial, or boundary data. Second, it yields exact-by-construction trainable shallow neural networks whose hidden units are themselves solutions of the governing equations, such as Maxwell’s equations or the wave equation. The main message is that symbolic structure can make scientific machine learning both more faithful and more efficient: rather than penalizing violations of PDEs after the fact, we learn directly in a computationally tractable space of exact solutions. We illustrate these ideas in applications to PDE solving, system control, and sampling from solution spaces.

[More...]

Reason with SAT For Rule Learning

Martina Seidl
Johannes Kepler University Linz, Austria

Propositional logic is one of the most successful formalisms in symbolic artificial intelligence. Many hard combinatorial problems can be naturally formulated as decision problems of propositional logic (SAT) and efficiently solved using modern SAT solvers. When using SAT, problems are described symbolically in a compact manner, in contrast to machine learning approaches, which typically rely on large volumes of data to characterize a problem.

In recent work, we have investigated how SAT techniques can be applied to learning tasks that involve examples. In this talk, we report on our experiences, examine the gap between symbolic and subsymbolic approaches, and outline potential directions for future research.

Learning-Based Complexity of PDE Solutions

Juan Esteban Suarez
Ludwig-Maximilians-Universität München, Germany

Partial Differential Equations (PDEs) are fundamental tools for modeling phenomena across physics, biology, and engineering, yet their numerical approximation becomes challenging in the presence of singularities, discontinuities, or complex geometries. While classical numerical methods—such as finite element, finite volume, and spectral schemes—offer strong theoretical guarantees, they typically rely on high regularity assumptions and scale poorly in non-smooth or high-dimensional settings. Recent advances in scientific machine learning have introduced new approximation paradigms based on variational formulations, neural representations, and hybrid surrogate models, raising fundamental questions about the computability and algorithmic complexity of PDE solutions.

In this talk, we explore how modern learning-based models can be used as computational structures for studying the computability and complexity of broad classes of PDE solutions, including those with singularities and discontinuities. We present a variational framework for analyzing the algorithmic complexity of a class of continuous PDE solutions using polynomial approximation schemes, and discuss extensions based on hybrid surrogate models that enable the analysis of discontinuous solutions. This framework provides constructive insights into the design of novel computational architectures for solving PDEs, addressing both the limitations of classical solvers and the energy-efficiency challenges of state-of-the-art AI models.

[More...]

Alien Codes and Their Automated and Human Explanations

Josef Urban
Czech Technical University in Prague, Czech Republic.

We have automatically discovered symbolic explanations for over one-third of the sequences in the Online Encyclopedia of Integer Sequences (OEIS). The talk will describe the neuro-symbolic system consisting of a positive feedback loop that starts from zero knowledge and iterates between guessing the explanations, their verification, and training of the guessing methods. Then I will describe several additions and experiments that led to the current set of solutions found in hundreds of iterations of the feedback loop. I will show some of the solutions discovered. This includes over 50 programs for primes developed as the system self-evolves. I will also discuss a related experiment in automatically proving equivalences of the discovered programs using the SMT solver Z3. Because induction is often needed in such proofs, this leads to another self-learning neuro-symbolic system that repeatedly tries to guess the right instances of induction for Z3. Finally, I will also show some of the recent human explanations of the programs, mostly done by Tom Hales.

[More...]

Getting Math from the Computational Universe

Stephen Wolfram
Wolfram Research, Champaign, USA

How does computation relate to the mathematics that humans have done, and are interested in? I'll talk about the science of the computational universe, and what it tells us about the foundations and future of mathematics, and what can and cannot be expected for mathematics from AI. I also expect to show some new technology under development, as well as some new science that addresses the foundations of machine learning and their relation to mathematics.

Contributed Talks

Invited Talks

Generate, Verify, Refine: A Closed-Loop LLM–CAS Approach to Symbolic Integration
Stav Belyy, Shalev Zuriel, Tomer Raz, Michael Shalyt, Ido Kaminer
Reactmine: a Statistical Tree-Search Algorithm for Learning Biochemical Reactions from Time Series Data
Constant Le Bezvoët, François Fages, Julien Martinelli
Towards Inductive Logic Programming at Scale
David M. Cerna
Improving Optimisation Formulations in Industrial Settings with LLMs
Tereso del Río
Interactive AI for Computer Algebra: A Documentation-Grounded Assistant for ore_algebra
Lixin Du
Machine Learning Symbolic Integration Algorithm Selection
Matthew England
Approach for the Network Configuration of Wireless Systems using RAG, Fine-Tuning and Formal Verification Component
Steffen Fricke, Jürgen Jasperneite
The Extended Scientific Method — From DNA to SC and ML
Erhard Glötzl
A Computational Framework for Automated Discovery within Conservative Matrix Fields
Uri Kasher Hitin, Michael Shalyt, Shachar Weinbaum, Hila Barkan, Tali Monderer, Elyasheev Leibtag, Rotem Kalisch, Ido Kaminer
On the Use of ChatGPT in Symbolic Computation and Mathematical Research: A Case Study in Computational Origami
Tetsuo Ida
Efficient Dataset Generation for Bases of Zero-Dimensional Ideals
Yuki Ishihara, Kazuhiro Yokoyama
Breaking the Data Barrier in Learning Symbolic Computation: A Case Study on Variable Ordering Suggestion for Cylindrical Algebraic Decomposition
Rui-Juan Jing, Yuegang Zhao, Changbo Chen
Replacing Heuristic Rule Ordering in Symbolic Integration with Learned Policies
Rohit John, Rashid Barket, Matthew England
Zariski-Dense Dataset Generation for Learning to Compute Gröbner Bases
Yuta Kambe
Comparing Human Perception, Computer-Algebra, and Generative AI Approaches for Ranking Elementary Geometry Statements
Zoltán Kovács, Tomás Recio, Piedad Tolmos, Pilar M. Vélez
Operator-Theoretic and Complexity-Based Synthesis of a Gradient-Free Federated Kernel Learner
Mohit Kumar, Bernhard A. Moser, Manuela Geiß
Verified Vibe Coding
Gábor Kusper
Deep Learning for Integro-Differential Modelling
François Lemaire, Louis Roussel
Towards Quantum-Reservoir Trajectory Signatures for Symbolic Rewriting Dynamics
Alexei Lisitsa
When the Vibes Fade: An Industry Perspective on LLM Coding Limits — A Discussion Case for Symbolic Computation
Thomas Mahringer
Discovering Symbolic Representation of Conservation Laws of Dynamical Systems using Machine Learning
Meskerem Abebaw Mebratie, Rüdiger Nather, Guido Falk von Rudorff, Werner M. Seiler
Proof Engineering: Nakano’s Light Puzzle Example
Koji Nakagawa, Bruno Buchberger
Representing Polynomial Ideals as Heterogeneous Graphs for Inductive Machine Learning
Rüdiger Nather
Reasoning over Legal Texts Using Large Language Models and Automated Reasoning
Verena Praher, Endre Szasz-Revai, Wolfgang Windsteiger
On the Rapid Prototyping of a Logical Agent
Wolfgang Schreiner
Exact Algebraic Computation of Learning Coefficients for Two-Dimensional Singular Models
Gregoire Sergeant-Perthuis, Jules Tsukahara, Elias Tsigaridas
Unifying Structure for Ramanujan’s 17 Series for 1/π: A Human-AI Discovery
Michael Shalyt, Elyasheev Leibtag, Shachar Weinbaum, Ido Kaminer
Certified CAS-assisted Polynomial Reasoning in Lean 4
Hao Shen, Junyu Guo, Junqi Liu, Lihong Zhi
Learning to Rank Symbolic Expressions for Model Selection
Ali Soltani, Gabriel Kronberger, Fabricio Olivetti de França, Alessandro Lucantonio
Learning to Compute Polynomial Products with Transformers
Yuxuan Song, Changbo Chen

Please consider subscribing to the SCML Mailing List in order to stay informed about the SCML-2026 conference.