Programme Overview

The conference organizers need your feedback. Please take a few minutes to participate in the following online survey.

All events (except banquet) take place in the conference hotel, One Washington Circle.
Detailed schedule by day: Monday, Tuesday , Wednesday , Thursday, Friday.

	Monday 13. July		Tuesday 14. July	Wednesday 15. July		Thursday 16. July	Friday 17. July
	Crescent Room	Meridian Room	Meridian Room	Crescent Room	Meridian Room	Meridian Room	Meridian Room
9:00	[D1] Daniel Szymczak. Literate Development of Families of Mathematical Models (Monday, 9:00-9:45, Crescent Room)		Short Presentations [R17] Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan-Afshar, Cvetan Dunchev and Sofiene Tahar. Formalizing Physics: Automation, Presentation and Foundation Issues (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R19] Umair Siddique, Osman Hasan and Sofiene Tahar. Towards the Formalization of Fractional Calculus in Higher-order Logic (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R20] Max Wisniewski, Alexander Steen and Christoph Benzmüller. LeoPARD --- A Generic Platform for the Implementation of Higher-Order Reasoners (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R21] Moa Johansson, Dan Rosén, Nicholas Smallbone and Koen Claessen. TIP: Tons of Inductive Problems (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R22] Ross Moore. Semantic Enrichment of Mathematics via `tooltips' (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R23] Kazuhisa Nakasho and Yasunari Shidama. Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R24] Adam Naumowicz. Tools for MML Environment Analysis (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R25] Ons Seddiki, Cvetan Dunchev, Sanaz Khan-Afshar and Sofiene Tahar. Enabling Symbolic and Numerical Computations in HOL Light (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [WIP4] Pedro Quaresma, Vanda Santos, Milena Marić. A Web Environment for Geometry (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [WIP5] Johan Commelin, Josef Urban. Auto-hyperlinking the Stacks Project (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [WIP6] Deyan Ginev, Mihnea Iancu, Constantin Jucovshi, Andrea Kohlhase, Michael Kohlhase, Jürgen Schefter, Wolfram Sperber. The SMGloM Project and System (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [Poster1] Nathan Carter, Ken Monks. A web-based word processor with mathematical semantics (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [Poster2] Manfred Minimair. Math Chat in Collaborative Computer Algebra Shells (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [Poster3] Michael Kohlhase, Florian Rabe. The OAF Project: An Open Archive of Formalizations (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)	[TH1] Pedro Quaresma. Visual Geometry Proofs in a Learning Context (Wednesday, 9:00-9:30, Crescent Room)	Introduction	[R15] Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk and Josef Urban. Mizar: State-of-the-art and Beyond (DOI) (Thursday, 9:00-9:45, Meridian Room)	9:00-10:30 and 11:00-12:30: Isabelle Tutorial Tobias Nipkow. Isabelle Tutorial (Friday, 9:00-10:30 and 11:00-12:30, Meridian Room)
9:05					[FM1] Cezary Kaliszyk. Invited talk: Learning to parse mathematics from aligned corpora (Wednesday, 9:05-9:50, Meridian Room)
9:30				[TH2] Richard R. Philippe. Argumentative Effects of a Geometric Construction Tutorial System in Solving Problems of Proof (Wednesday, 9:30-10:00, Crescent Room)
9:45	[D2] Dennis Müller. Knowledge Management across Formal Libraries (Monday, 9:45-10:30, Crescent Room)	[MA1] Davide Cervone, Peter Krautzberger, Volker Sorge. Towards Meaningful Visual Abstraction of Mathematical Notation (Monday, 9:45-10:30, Meridian Room)				[R18] Claudio Sacerdoti Coen and Ferruccio Guidi. A Survey on Retrieval of Mathematical Knowledge (DOI) (Thursday, 9:45-10:30, Meridian Room)
9:50					[FM2] Dennis Müller, Michael Kohlhase. Understanding Mathematical Theory Formation via Theory Intersections in MMT (Wednesday, 9:50-10:10, Meridian Room)
10:00				[TH3] Crispin Perdue. Creating Usable Computer Tools that Reason Mathematically (Wednesday, 10:00-10:30, Crescent Room)
10:10					[FM3] Marco Maggesi. A symbolic approach to abstract algebra in HOL Light (Wednesday, 10:10-10:30, Meridian Room)
10:30	Coffee next to Zenith Room		Coffee next to Zenith Room	Coffee next to Zenith Room		Coffee next to Zenith Room	Coffee next to Zenith Room
11:00	[D3] Daniel Selsam. Free and infinitely scalable advanced mathematics education (Monday, 11:00-11:45, Crescent Room)	[MA2] Deyan Ginev, Nathan Jenkins,Alberto Pepe. Live Mathematics in Authorea: Data, Computation and Visualization (Monday, 11:00-11:45, Meridian Room)	Poster Session Zenith Room [R17] Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan-Afshar, Cvetan Dunchev and Sofiene Tahar. Formalizing Physics: Automation, Presentation and Foundation Issues (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R19] Umair Siddique, Osman Hasan and Sofiene Tahar. Towards the Formalization of Fractional Calculus in Higher-order Logic (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R20] Max Wisniewski, Alexander Steen and Christoph Benzmüller. LeoPARD --- A Generic Platform for the Implementation of Higher-Order Reasoners (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R21] Moa Johansson, Dan Rosén, Nicholas Smallbone and Koen Claessen. TIP: Tons of Inductive Problems (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R22] Ross Moore. Semantic Enrichment of Mathematics via `tooltips' (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R23] Kazuhisa Nakasho and Yasunari Shidama. Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R24] Adam Naumowicz. Tools for MML Environment Analysis (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [R25] Ons Seddiki, Cvetan Dunchev, Sanaz Khan-Afshar and Sofiene Tahar. Enabling Symbolic and Numerical Computations in HOL Light (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [WIP4] Pedro Quaresma, Vanda Santos, Milena Marić. A Web Environment for Geometry (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [WIP5] Johan Commelin, Josef Urban. Auto-hyperlinking the Stacks Project (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [WIP6] Deyan Ginev, Mihnea Iancu, Constantin Jucovshi, Andrea Kohlhase, Michael Kohlhase, Jürgen Schefter, Wolfram Sperber. The SMGloM Project and System (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [Poster1] Nathan Carter, Ken Monks. A web-based word processor with mathematical semantics (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [Poster2] Manfred Minimair. Math Chat in Collaborative Computer Algebra Shells (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room) [Poster3] Michael Kohlhase, Florian Rabe. The OAF Project: An Open Archive of Formalizations (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)	[TH4] Crispin Perdue. Mathtoys Demo (Wednesday, 11:00-12:00, Crescent Room)	[FM4] Marco Maggesi. A formalisation of metric spaces in HOL Light (Wednesday, 11:00-11:20, Meridian Room)	[R12] Karol Pąk. Readable Formalization of Euler's Partition Theorem in Mizar (DOI) (Thursday, 11:00-11:30, Meridian Room)	9:00-10:30 and 11:00-12:30: Isabelle Tutorial Tobias Nipkow. Isabelle Tutorial (Friday, 9:00-10:30 and 11:00-12:30, Meridian Room)
11:20					[FM5] Adam Naumowicz. Formalizing Divisibility Rules as a Student Case Study (Wednesday, 11:20-11:40, Meridian Room)
11:30						[R13] Daniel Raggi, Alan Bundy, Gudmund Grov and Alison Pease. Automating change of representation for proofs in discrete mathematics (DOI) (Thursday, 11:30-12:00, Meridian Room)
11:40					[FM6] Mario Carneiro. GCH implies AC, a Metamath Formalization (Wednesday, 11:40-12:00, Meridian Room)
11:45	[D4] Waqar Ahmed. Formal Reliability Analysis using Higher-order Logic Theorem Proving (Monday, 11:45-12:30, Crescent Room)	[MA3] Michael Kohlhase, Sourabh Lal, Tom Wiesing, Deyan Ginev. KAT: an Annotation Tool for STEM Documents (Monday, 11:45-12:30, Meridian Room)
12:00					[FM7] Karol Pąk. Improving Legibility of Proof Scripts in Mizar (Wednesday, 12:00-12:20, Meridian Room)	[R14] Qun Zhang and Abdou Youssef. Performance Evaluation and Optimization of Math-Similarity Search (DOI) (Thursday, 12:00-12:30, Meridian Room)
12:20					[FM8] Closing discussion (Wednesday, 12:20-12:30, Meridian Room)
12:30	Lunch (on your own)		Lunch (on your own)	12:30/13:00-15:00: Lunch Banquet at Hill Country Barbecue Market DC (joint walk/travel, banquet starts 13:00) Lunch Banquet at Hill Country Barbecue Market DC (joint walk/travel, banquet starts 13:00) (Wednesday, 12:30/13:00-15:00, Hill Country Barbecue Market)		Lunch (on your own)	Lunch (on your own)
14:00	[Invited Talk Jim Pitman] Jim Pitman. Towards a Global Digital Mathematics Library (Monday, 14:00-15:00, Meridian Room) Meridian Room		[Invited Talk Richard Zanibbi] Richard Zanibbi (with Awelemdy Orakwue). Math Search for the Masses: Multimodal Search Interfaces and Appearance-Based Retrieval (DOI) (Tuesday, 14:00-15:00, Meridian Room)			[Invited Talk Tobias Nipkow] Tobias Nipkow (with Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk). Mining the Archive of Formal Proofs (Thursday, 14:00-15:00, Meridian Room)	[Invited Talk Leonardo de Moura] Leonardo de Moura. Formalizing mathematics using the Lean Theorem Prover (DOI) (Friday, 14:00-15:00, Meridian Room)
14:30
15:00	[D5] Discussion: How to give an effective presentation (Monday, 15:00-16:00, Crescent Room)	[MA4] Naomi Pentrel, Michael Kohlhase. Relational Presentation Using Semantic Closeness (Monday, 15:00-15:45, Meridian Room)	[R7] Mihnea Iancu and Michael Kohlhase. A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics (DOI) (Tuesday, 15:00-15:30, Meridian Room)	15:00-: Possibility to visit Smithsonian Museums (on your own) Possibility to visit Smithsonian Museums (on your own) (Wednesday, 15:00-, Smithsonian Museums)		[R1] Waqar Ahmed and Osman Hasan. Towards Formal Fault Tree Analysis using Theorem Proving (DOI) (Thursday, 15:00-15:30, Meridian Room)	[R5] Florian Rabe. Generic Literals (DOI) (Friday, 15:00-15:30, Meridian Room)
15:30			[R8] Serge Autexier and Dieter Hutter. Structure Formation in Large Theories (DOI) (Tuesday, 15:30-16:00, Meridian Room)			[R2] Luís Cruz-Filipe and Peter Schneider-Kamp. Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof (DOI) (Thursday, 15:30-16:00, Meridian Room)	[R6] Paul Tarau. Ranking/unranking of Lambda Terms with Compressed de Bruijn Indices (DOI) (Friday, 15:30-16:00, Meridian Room)
15:45
16:00	Coffee next to Zenith Room		Coffee next to Zenith Room			Coffee next to Zenith Room	Coffee next to Zenith Room
16:30	[D6] Daniel Raggi. Change of representation in discrete mathematics (Monday, 16:30-17:15, Crescent Room)	[MA5] Philippe R. Richard, Michel Gagnon and Josep Maria Fortuny. Interactive management of problems in geometry for the development of student skills and the acquisition of mathematical knowledge (Monday, 16:30-17:15, Meridian Room)	[R9] Fulya Horozal and Florian Rabe. Formal Logic Definitions for Interchange Languages (DOI) (Tuesday, 16:30-17:00, Meridian Room)			[R3] Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov. A First Class Boolean Sort in First-Order Theorem Proving and TPTP (DOI) (Thursday, 16:30-17:00, Meridian Room)	[WIP1] Bob Neveln, Bob Alps. Parsing Texts and Checking Proofs in LaTeX (Friday, 16:30-17:00, Meridian Room)
17:00			[R10] Mihnea Iancu and Michael Kohlhase. Math Literate Knowledge Management via Induced Material (DOI) (Tuesday, 17:00-17:30, Meridian Room)			[R4] Steven Obua, Jacques Fleuriot, Phil Scott and David Aspinall. Type Inference for ZFH (DOI) (Thursday, 17:00-17:30, Meridian Room)	[WIP2] Mario Carneiro. Arithmetic in Metamath, Case Study: Bertrand's Postulate (Friday, 17:00-17:30, Meridian Room)
17:15	[D7] Individual discussions with mentors (Monday, 17:15-18:00, Crescent Room)	[MA6] Andrea Kohlhase and Ana Guseva:. Co-Occurrences of Context Dimensions of Spreadsheets (Monday, 17:15-18:00, Meridian Room)
17:30			[R11] Bruce Miller. Strategies for Parallel Markup (DOI) (Tuesday, 17:30-18:00, Meridian Room)			17:30-18:30: Business Meeting Business Meeting (Thursday, 17:30-18:30)	[R16] Howard Cohl, Moritz Schubotz, Marjorie McClain, Bonita Saunders, Cherry Y. Zou, Azeem S. Mohammed and Alex A. Danoff. Growing the Digital Repository of Mathematical Formulae with Generic LaTeX Sources (DOI) (Friday, 17:30-18:00, Meridian Room)
18:00		[MA7] Tool Demonstrations (Monday, 18:00-19:00, Meridian Room)	[WIP3] Théo Zimmermann, Hugo Herbelin. Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant (Tuesday, 18:00-18:30, Meridian Room)
18:30

Legend										Free
Calculemus	Digital Mathematical Libraries (DML)	Doctoral Program	Formal Mathematics for Mathematicians (FM4M)	Tutorial	Mathematical Knowledge Management (MKM)	MathUI	Projects & Surveys	Systems & Data	Theorem Provers Components for Educational Software (ThEdu)	Work-In-Progress

News
- Please participate in the online survey
- Work-in-Progress informal proceedings online
- Springer proceedings available online
- Travel information available

Last modified: December 18 2025 12:45:30 CET

Programme Overview

The conference organizers need your feedback. Please take a few minutes to participate in the following online survey.

News