PROGRAM
Days: Monday, September 21st Tuesday, September 22nd Wednesday, September 23rd Thursday, September 24th Friday, September 25th
Monday, September 21st
View this program: with abstractssession overviewtalk overview
Tuesday, September 22nd
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 5: Invited Talk
Invited Talk
Chair:
| 09:00 | Using theorem provers to reason about money: the act verification framework for Ethereum smart contracts (abstract) |
10:30-12:00 Session 6
Chair:
| 10:30 | Distilling Autoformalized Proofs (abstract) |
| 11:00 | Optimising Metamath Proofs for Human Working Memory (abstract) |
| 11:30 | Modeling Learner Competencies: Does Mathematical Knowledge Management Have an Influence? (abstract) |
13:30-14:30 Session 7: Invited Talk
Invited Talk
Chair:
| 13:30 | Semantic Alignment Models: A Bridge Between Informal and Formal Mathematics |
14:30-15:00 Session 8
Chair:
| 14:30 | Formalizing How Concepts are Expressed in Natural Language (abstract) |
| 14:45 | Publication-Coordinate Audit Interfaces for AI-Assisted Formal-Mathematics Pipelines (abstract) |
15:30-17:30 Session 9
Chair:
| 15:30 | Toward Satisfiability Modulo Realizability (abstract) |
| 16:00 | Vampire Guide: An Interactive Playground for Learning and Teaching about Vampire (abstract) |
| 16:20 | OpenProver: Agentic and Interactive Theorem Proving with Lean 4 (abstract) |
| 16:40 | Learning-Guided Higher-Order Automated Reasoning for Isabelle/HOL (abstract) |
| 17:00 | A project report on proof data extraction, interaction, and evaluation in Isabelle (abstract) |
Wednesday, September 23rd
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 10
Chair:
| 09:00 | Knowledge management in House of Graphs (abstract) |
| 09:30 | Maniplexes as a Foundation for Cross-Linked Databases of Symmetric Objects (abstract) |
10:30-12:00 Session 11
| 10:30 | A Combinatorial Rewriting Model for Origami (abstract) |
| 11:00 | IntSeqBERT: Learning Arithmetic Structure in OEIS via Modulo-Spectrum Embeddings (abstract) |
| 11:30 | A Toolbox for Undefined Terms in Type Theory (abstract) |
13:30-14:50 Session 12
Chair:
| 13:30 | Categorizing Mathematical Concepts with LLM Voting Ensembles in Mathswitch (abstract) |
| 14:00 | Identifying Dependencies in Mathematical Data via Predictive Importance (abstract) |
| 14:30 | Automorphism group certificates for cubic vertex-transitive graphs (abstract) |
Thursday, September 24th
View this program: with abstractssession overviewtalk overview
10:30-11:40 Session 15
Chair:
| 10:30 | Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery (abstract) |
| 11:00 | A Context-Free Parser of Math Expressions (abstract) |
| 11:20 | System Description: Natty 0.5 (abstract) |
Friday, September 25th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 16: Invited Talk
Invited Talk
Chair:
| 09:00 | Type theory for discrete mathematics (abstract) |
10:30-12:30 Session 17
Chair:
| 10:30 | Formalising Continued Fractions (With Applications to Pell's Equation) (abstract) |
| 11:00 | Formalising Hilbert Polynomials in Lean (abstract) |
| 11:30 | Formalizing Soundness and Consistency of Q0 (abstract) |
| 12:00 | A Formal Analysis Framework for Linear Partial Differential Equations in HOL (Project Paper) (abstract) |