CICM 2025 Invited Speakers

• Fabian Huch, Technische Universität München (TUM)
  Keynote Supporting Maintenance of Formal Mathematics with Similarity Search
  Abstract Maintaining large formal mathematics libraries is labor intensive. We propose methods to reduce this effort by exploiting structural similarity: First, we detect duplicates by combining syntax, markup, and formula structure, using a scalable discriminator-based approach that achieves perfect precision on Isabelle/HOL up to a 0.95 similarity threshold. Second, we identify proper locations for auxiliary lemmas via community detection on dependency graphs, suggesting the correct location within the top 6 neighborhoods on average (median).
  Bio Fabian Huch is a young researcher who earned his B.Sc. and M.Sc. at the Technische Universität München, where he joined the theorem proving group in 2020. His research focuses on computer support for large-scale Mathematics, which he advances as a developer of the Isabelle system. He is also passionate about the Archive of Formal Proofs: Both as a treasure trove of formalized mathematics and as an invaluable body of research. When not behind a keyboard, he enjoys cooking and tinkering on one of his DIY projects.
• Assia Mahboubi, INRIA, Nantes
  Keynote Formal proofs: computer science at the service of rigour and creativity in mathematics
  Abstract For more than half a century, computers have become essential research instruments in many different areas of fundamental mathematics. They have dramatically expanded the scale of experimentation and visualization in mathematics, becoming this way precious assistants for shaping conjectures. But also for finding proofs. This talk proposes to discuss the role of computer tools in contemporary mathematics, and in particular the potential impact of the rise of interactive theorem proving and of the advent of large corpora of mathematics machine-checked with provers like Rocq, Lean, Isabelle, Agda, etc.
  Bio Assia Mahboubi is a tenured researcher (directrice de recherche) at Inria, in the Gallinette team, Nantes, France. She's also an endowed professor in the Algebra and Number Theory section of the Vrije Universiteit Amsterdam, in the Netherlands. Her research interests revolve around the foundations and formalization of mathematics in type theory and the automated verification of mathematical proofs. She's especially interested in the interplay between computer algebra and formal proofs and, more generally, in computer-aided mathematics, using the Rocq interactive proof assistant.
• Daniele Nantes Sobrinho, University of Brasilia (UnB)
  Keynote Equational Reasoning in Program Verification
  Abstract Several successful analysis tools and platforms support compositional verification and/or compositional bug-finding for heap-manipulating programs. These approaches are often powered by compositional symbolic execution (CSE), grounded in ideas from separation logic (SL) and incorrectness separation logic (ISL). In this context, “compositional” means that the analysis scales by reasoning about functions in isolation—anywhere in the codebase—producing simple function specifications that can be reused in broader calling contexts. Modern CSE-based tools rely critically on two capabilities: reasoning about function calls using function specifications, and manipulating user-defined predicates. A key challenge that arises here is the frame inference problem (FIP): determining which parts of the symbolic state are relevant for a given operation. Many tools address FIP using a consume-produce approach, which reduces the problem to a form of matching between logical assertions and symbolic states. In this talk, I will argue that the FIP—and, more broadly, symbolic analysis in this setting—is inherently an equational problem. Reasoning modulo axioms, while often necessary, introduces a significant burden that must be carefully managed in both the formalisation and implementation of these analyses. (Joint work with Andreas Lööw, Philippa Gardner and Simon Park.)
  Bio Daniele Nantes Sobrinho is a Research Fellow at the Verified Software Group at Imperial College London and an Adjunct Professor (on research leave) at the University of Brasília, where she has been part of the Department of Mathematics since 2016. She holds a PhD in Mathematics from the University of Brasília (2013) and has extensive experience in theoretical computer science, formal methods, and automated reasoning. Her research collaborations span multiple institutions worldwide, including King’s College London, Groningen University and Goethe-University Frankfurt. She has has contributed to advancements in nominal techniques, rewriting systems, symbolic computation, and logic-based software verification. Daniele is an active member of the international research community, serving on steering committees and program committees for conferences such as FSCD, LSFA, and UNIF. She has also organized workshops and initiatives promoting diversity, equity, and inclusion in STEM, including the Women in Logic (WiL) workshop and the DEI4Everyone initiative at POPL 2024.
• Josef Urban, Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC)
  Keynote Alien Codes and Their Automated and Human Explanations
  Abstract 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.
  Bio Josef Urban is a distinguished researcher at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC), heading its AI department and formerly also the ERC project AI4REASON. His main interests are in combining inductive/learning and deductive/reasoning AI methods over large formal mathematical corpora. His systems have won several theorem proving competitions, and the methods today assist formal verification in proof assistants. He received his MSc in Mathematics and PhD in Computer Science from Charles University in Prague, worked as an assistant professor in Prague, and as a researcher at University of Miami and Radboud University Nijmegen. He has also co-founded the conference on Artificial Intelligence and Theorem Proving (AITP) and co-organized it since 2016.

Joint Invited Speaker with LSFA 2025:

• Temur Kutsia, Research Institute for Symbolic Computation (RISC), Johannes Kepler University
  Keynote Solving Symbolic Constraints
  Abstract Symbolic constraint solving is a fundamental technique in many areas of mathematics and computer science, providing the basis for key operations in automated reasoning, term rewriting, declarative programming, or formal methods. Important classes of symbolic constraints include unification, matching, generalization, disunification, ordering constraints. Efficient methods for solving them form the computational core of inference engines, proof assistants, program transformation systems, logical frameworks, etc. In this talk, we present recent advances in solving unification, matching, and generalization constraints in expressive theories, including those that involve background knowledge or binding constructs. We discuss algorithmic techniques for constraint solving, identify classes of problems that admit efficient solutions, and highlight their relevance for tools and techniques in symbolic computation and computer mathematics.
  Bio Temur Kutsia obtained his PhD and habilitation in mathematics from Johannes Kepler University Linz, where he is currently a senior researcher at the Research Institute for Symbolic Computation (RISC). His work covers various aspects of computational logic and symbolic AI, including unification and generalization, declarative programming, automated reasoning, rewriting, and their applications. He has published over 100 papers on these topics, contributed to the development of software packages, and led several research projects.