Formalizing all indexed mathematics as a benchmark for general reasoning, with the example of implementing dilatations of categories

A. Mayeux

Formal rigor distinguishes mathematics from other disciplines, in the sense that mathematical statements are derived from explicit axioms by logically verifiable steps. Interactive…