Mathematical Knowledge Management Survey Paper Review

Mathematical_Knowledge_Management.txt

This is my notes to the paper presented in the video

https://youtu.be/Pp85jeBCDmc

And here's some of the other links shown in the video:

https://en.wikipedia.org/wiki/Mathematical_knowledge_management

https://arxiv.org/pdf/1912.03028.pdf (A Survey on Theorem Provers in Formal
Methods)

http://www.cas.mcmaster.ca/sqrl/papers/SQRLreport18_rev2.pdf (The Seven Virtues of Simple Type Theory)




# Title

* "The Space of Mathematical Software Systems — A Survey of Paradigmatic Systems"
* 12 Feb 2020
* https://arxiv.org/abs/2002.04955
* Living document
* Also essentially unfinished at this point.

# About the authors
* Main author
https://en.wikipedia.org/wiki/Michael_Kohlhase
    * MKM
        - https://en.wikipedia.org/wiki/Mathematical_knowledge_management
    * worked on Math markup languages
        - https://en.wikipedia.org/wiki/MathML
        - https://en.wikipedia.org/wiki/OpenMath
arxiv
    * https://arxiv.org/search/cs?searchtype=author&query=Kohlhase%2C+M
    * Two previous papers on arxiv with Farmer.
        - Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal
            + Similar content to this paper
        - Realms: A Structure for Consolidating Knowledge about Mathematical Theories
            + More formal

# Motivation to read
Note: I came across the work of William M. Farmer in Canada
years ago when learning lambda calculus and type system.
I know he's been working on this kind of thing.

# Questions pre-read (200513)
* How do MKM (Mathematical Knowledge Management) Systems differ?
* What's the timeline of the various approaches?
* What are some new ideas?
* Who is working on this?

# Table of Contents
## 1 Introduction 3
## 2 Primary Aspect: Inference 4
## 3 Primary Aspect: Computation 7
## 4 Primary Aspect: Concretization 8
## 5 Primary Aspect: Narration 11
## 6 Primary Aspect: Organization 14
## 7 The Big Table of Systems and their Aspects 15
## 8 Realizing Secondary Aspects 18
## 9 Conclusion

# Notes
## 1 Introduction 3
Highlights the evergrowing amount of mathematical knowledge out there and that
computerization is natural/inevitable in ORGANIZATION of it.
Proposes that there are 4 features that a good organizing framework must poses.
Claims that current systems largely only focus on one.
The 4 features and their representatives (in the sense above) are discussed in the following chapters.
## 2 Primary Aspect: Inference 4
Differences are roughly explained and examples given for:
    * Proof assistants
        - Tend to have stronger logics than what is assumed in textbooks.
        - Tradeoff between flexibility & ease of use of logic vs. typing & computational power.
        - Mention aspects of software architecture up to human-user interface
        - Implement logic and provide libraries
    * automated theorem provers
        - Usually simpler logics where automation is feasible
    * Satisfiability checkers
        - More limited scope
Speciifically, more computational aspects are discussed for:
    * Terminating recursion
        - termination checkers
    * Rewriting
        - https://en.wikipedia.org/wiki/Rewriting
        - implements a directed equality relation
        - Various systems have rewriting features
    * Logic programming
        - "works well with Axioms in Horn-form"
            + https://en.wikipedia.org/wiki/Horn_clause
        - "mostly investigated in untyped first-order logic via various Prolog dialects"
## 3 Primary Aspect: Computation 7
Further subdivided into
    * Typed
        - Dependent type theory
    * Symbolic
        - Abstract syntax trees
            + Hard to combine wiht TT
    * Algebraic
        - For algebra in a broad sense
    * Numeric (analytic & statistical)
        - For "reals"
## 4 Primary Aspect: Concretization 8
Historical examples: Pythagorean triples, lists of decimal digits of pi, logarithm tables.
Aspects:
    * Encodings
        - Discussion of semantics of concrete objects, encoding and decoding
    * Data and Knowledg
        - Reports of some database sizes (e.g. in TB ranges)
        - "Commonly occurring themes in mathematical data are ad-hoc implementations of codecs, lack of community guidelines for data, and similar."
    * Record Data (R)
    * Array Data (A)
    * Linked Data (L)
        - Knowledge graphs and metadata
    * Isomorphism Classes (I)
    * Redundant Information/Computed Properties (P)
    * Complete Enumeration (E)
    * Integration with Computation System (C)
    * Standalone Databases
    * Data Sets within Computation Systems
## 5 Primary Aspect: Narration 11
Standard texts from human for humans (also explains intuition, etc).
Classification into 5 types (dubbed RL0-RL4).
Discusses presentation languages and translatability, depending on formality level.
    * At the Presentational Level (P): Word Processors & Document Preparation Systems
        - Discusses drawback, for searchability, of having TeX be converted to images
    * Formal, Narrative Documents (F)
        - Reports of systems that try to merge the formal capturing with the narravite capturing of math
        - Reports of human-readable side-output (as in the Mizar mag.)
    * Semi-Formal Systems (S): Documents at the Semantic Level
        - "flexiformal mathematics"
        - Mixed formats like Mathematica & Jupyter
## 6 Primary Aspect: Organization 14
Types or aspects of organization:
    * Compound Units of Mathematical Knowledge (C)
    * Indexed Knowledge Collections (I)
        - Examples: Soft/Informal knowledge on websites
    * Graph-Structured/Semantic Organization (G)
        - Discussion the notion of "theory graphs"
    * Heterogeneous Organization (H)
    * Formal Organization (F)
    * Organization by Mathematical Practice (P)
        - Math Subject Classifica- tion
    * Explicitly represented mathematical knowledge
## 7 The Big Table of Systems and their Aspects 15
Some (Most?) examples categorized.
The authors point out that the 4 (5) categories overlap.
## 8 Realizing Secondary Aspects 18
Talks about that it's common for system to have narrative aspects as supplement
(documentation-like extra information).
## 9 Conclusion

# Related
* Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal
https://arxiv.org/abs/1904.10405
* A Survey on Theorem Provers in Formal Methods
https://arxiv.org/pdf/1912.03028

# Thoughts
Missing:
  * GroupProps (https://groupprops.subwiki.org/wiki/Main_Page)
  * Cantors Attic (http://cantorsattic.info/Cantor%27s_Attic)