degrees of formalization in math

Update 2021-07-30: this concept is the de Bruijn factor.

There are many different views of formalization for mathematics. They are not all competing in the same scope. There are different degrees of formalization. Three analogies for this are

• spectrum of formalization, from informal (e.g., Latex) to increasing formality, like CAS and then to Proof assistants.
• "levels of zoom" as in visualization, like Google Maps but for Math
• compiling "high level concepts" (e.g., Latex) to controlled natural language to proofs

The idea of "zooming visualization" is relevant to the user experience -- a reader should be able to select the level of granularity.

The idea of "compiling" is about making implicit concepts explicit. Also, compiling to different architectures is similar to formalizing in different logics and axioms. Unlike the visualization concept, there is not one underlying basis to specify formalization in.


What are the degrees of formalization in math?

1. verbal (hallway chats, post-conference dinners, coffee breaks)
2. white board or chalk board
3. physical paper + pen or pencil
4. typesetting: Latex or equivalents like Markdown or pretextbook.org (XML based) or pandoc; Powerpoint; Rmd, reStructuredText, MyST, jupyterbook
5. semantic enrichment/decoration: sTeX, OMDoc; PDG inference rules; pf2 package (sty)
6. controlled natural languages (e.g., Naproche)
7. CAS verification of inference rules (e.g. Sage, SymPy)
8. formal verification in a selected target logic and axioms (e.g., Lean, Isabella, COQ)

References

https://arxiv.org/pdf/2005.12876.pdf and https://easychair.org/smart-slide/slide/1rfW# 

from https://physicsderivationgraph.blogspot.com/2020/07/notes-from-cicm-2020-13th-conference-on.html