recent work in math knowledge rep 2021Q3
2021-Q3 survey of recent work in math knowledge rep
Background definitions and motives
- FAIR Data: (wikipedia) data which meet principles of findability, accessibility, interoperability, and reusability.
- go-fair principles in more depth
Some surveys
- (Deep) FAIR Mathematics - (KWARC) 2020-02-25 by Katja Berčič, Michael Kohlhase, Florian Rabe
- "Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge" by Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe
- Expanded group from McMaster + KWARC shared working notes and tables as of 2020-Feb in:
"The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems" - A Survey of Languages for Formalizing Mathematics - (KWARC) 2020 by Cezary Kaliszyk and Florian Rabe
Some proceedings
- Accepted Papers at ITP2021 -- 12th International Conference on Interactive Theorem Proving
- ITP2021 Proceedings as a single PDF
- CADE 2021 Proceedings (open access at Springer) 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021
- CICM 2021 Proceedings (semi-browsable at Springer) of Intelligent Computer Mathematics 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021,
Some libraries and datasets
- Results of the First Phase of the OAF Project 2021-01-18 Michael Kohlhase, Florian Rabe
- Experiences from Exporting Major Proof Assistant Libraries Michael Kohlhase, Florian Rabe
- Making Isabelle Content Accessible in Knowledge Representation Formats Michael Kohlhase, Florian Rabe, Makarius Wenzel
- 10 Years Later: The Mathematics Subject Classification and Linked Open Data (arXiv preprint 2021-08-02) Susanne Arndt, Patrick Ion , Mila Runnwerth, Moritz Schubotz, and Olaf Teschke
Some nascent languages
- Towards a Heterogenous Query Language for Mathematical Knowledge (2020) Katja Berčič, Michael Kohlhase, Florian Rabe
- The Isabelle/Naproche Natural Language Proof Assistant ((2021, open access at Springer) De Lon A., Koepke P., Lorenzen A., Marti A., Schütz M., Wenzel M.
- A Language with Type-Dependent Equality (2021) Florian Rabe
Some online tools
- MathWebSearch search the nLab website using formulae with variables (following MathML / LaTeX)