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

https://cicm-conference.org/2020/cicm.php

The schedule is https://easychair.org/smart-program/CICM-13/

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

Monday

Joe Wells: slides for this talk are on Ciarán's web page: https://www.macs.hw.ac.uk/~cmd1/assets/talks/cicm-2020-talk.pdf
There is also a nearly-identical preprint on arxiv: https://arxiv.org/pdf/2005.13954.pdf
The machine-checked proofs that the axioms of zfp hold in the model we build for it can be found at: https://www.macs.hw.ac.uk/~cmd1/cicm2020/ZFPDoc/ZFP.html

Hanna Lachnitt: https://youtu.be/nbwZ-521sMQ

Tuesday

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
				Isabelle

<-- 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.
https://github.com/adelon/nave - written in Haskell

Guided tour of Formally verified constraint solvers :: Catherine Dubois

bugs have been found in constraint programming