Email Gateway (Jul 31 2025 at 19:27): Email Gateway (Jul 31 2025 at 19:27):From: Lucy Horowitz <cl-isabelle-users@lists.cam.ac.uk>
Call for Papers: ALIGN2025 <https://sites.google.com/view/align2025?usp=sharing> — Workshop on Alignments and Comparisons of Math Libraries and Datasets
Held in association with the 18th Conference on Intelligent Computer Mathematics (CICM 2025 <https://cicm-conference.org/2025/cicm.php>), University of Brasilia (Brasilia, Brazil), 6-11th October, 2025.
Submission deadline: rolling submissions until August 28, 2025
Workshop date: October 11, 2025 (TBC)
ALIGN 2025 invites contributions on the alignment, comparison, and cross-referencing of mathematical concepts across systems, formats, and representations. This includes identifying when two formalizations in different proof assistants refer to the same theorem, connecting informal mathematical exposition to formal counterparts, and more broadly, clarifying what it means to “mean the same thing” across divergent mathematical sources.
Alignments of this kind will support more interoperable proof systems, better search tools, and autoformalization efforts.
Topics of interest include (but are not limited to):
Dataset construction/annotation for aligned math corpora
Techniques for aligning formal and informal systems
Techniques for aligning different formal systems
Philosophical and practical considerations about the identity of mathematical concepts
Tooling for search or translation between systems
Early-stage projects, speculative ideas, and live demos are encouraged
Submissions may take the form of short papers/abstracts (up to 4 pages) or project demo proposals. Please send submissions to lucyhorowitz@berkeley.edu <mailto:lucyhorowitz@berkeley.edu>.
Important Dates
Paper submission deadline: Rolling submissions until August 28th, 2017
Author notification: September 5th, 2025
Workshop: 11th October 2025 (TBC)
Organizing Committee
Lucy Horowitz <https://math.berkeley.edu/~lucy/> (UC Berkeley, USA)
Valeria de Paiva <http://vcvpaiva.github.io/> (Topos Institute, USA)
Florian Rabe <https://kwarc.info/people/frabe/> (University of Erlangen, Germany)
Last updated: Aug 20 2025 at 20:23 UTC