Physics Derivation Graph navigation Sign in

Notes from CICM 2020 - 13th Conference on Intelligent Computer Mathematics

Published 2020-07-28T14:41:00Z by Physics Derivation Graph

The schedule is

The list below is incomplete since I didn't attend every presentation.


Joe Wells: slides for this talk are on CiarĂ¡n's web page:
There is also a nearly-identical preprint on arxiv:
The machine-checked proofs that the axioms of zfp hold in the model we build for it can be found at:

Hanna Lachnitt:


Survey of languages for formalizing math :: Cezary Kaliszyk

Observation: The language of formal systems is not the way mathematicians actually communicate (in person verbally, in writing).
Computer Algebra Systems (CAS) and Proof Assistants are viewed as "code" separate from Natural Language.

Natural Language Processing (NLP) of math does not recognize repeated use of the same notation, whereas humans recognize that as a convention.

Aspects that distinguish formal from informal communication: types, inheritance, equality (isomorphism). Each of those aspects are typically implicit for human consumers.
The goal of formal specification is proof, whereas in informal communication the goal is to convince the reader. Those are distinct.

Spectrum of math language formality:
natural language presentation semantic controlled natural languages proof assistants
speaking Latex CAS ForTheL Coq
written text presentation MathML sTeX Mizar Lean
<-- more informal        //       more formal -->

Observation: formal language can be more concise than Controlled Natural Language due to possibility of autocompletion in formal languages.

Cezary expects deep learning to be useful in translation from informal to formal languages, though the capability seems to vary.

Representing Structural Language features in formal meta languages :: Dennis Muller

MMT is defined in a 2013 Kohlhase paper "A scalable module system"
MMT is for math theories.

Formalization of Elementary Number Theory in Mizar :: Adam Naumowicz

Mizar has 60,000 theorems and 12,000 definitions in 1300 files.
Mizar is based on set theory.

The focus of this talk is the first 10 problems from the 1970 textbook by Sierpinski.

Question from audience: when will Mizar be open source?
Adam has no problem with open sourcing Mizar.
The specific barrier is not clear to me.

Interpreting Math texts in Naproche-SAD :: Peter Koepke

Naproche = Natural Proof Checking
SAD = System of Automated Deduction

The origin of Mizar is in a 1985 paper "Computer Aided Reasoning" by Blair and Trybulec

Integrating ForTheL with Latex :: Adrian De Lon

technique is to separate Latex text from math Latex and then develop separate grammars. - written in Haskell

Guided tour of Formally verified constraint solvers :: Catherine Dubois

bugs have been found in constraint programming