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

https://cicm-conference.org/2020/cicm.phpThe schedule is https://easychair.org/smart-program/CICM-13/

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: 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

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 |

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

MMT is defined in a 2013 Kohlhase paper "A scalable module system"

MMT is for math theories.

Mizar is based on set theory.

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

Adam has no problem with open sourcing Mizar.

The specific barrier is not clear to me.

SAD = System of Automated Deduction

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

https://github.com/adelon/nave - written in Haskell