I will be following your work at http://axiommath.ai closely. Since I've been working on Axiom (computer algebra) since the 1980s I have opinions :-)
The connection betwen Types and mathematical Definitions is worth capturing. While trying to merge Axiom and LEAN I spent a fair amount of time thinking about ways to capture Types. It seems to me that Types are most useful when they are organized to support Definitions. For example, the type Continuous captures that a function is continuous at a point if the limit as you approach that point equals the actual function's value at that point, with the limit existing and being the same from both sides. Of course, that assumes a Type capturing the definition of Limit, etc. This attempt at capturing Definitions as Types was the basis of the SANE Axiom effort. >From my continuous (pun intended) scratching at the problem I found whole textbooks [0][1] that undermine any Type based on a definition. The whole effort bogged down in so much complexity I gave up. To contruct a "correct" Type tower in any sub-field you need to be an expert in that sub-field. Unfortunately the constructed Type tower in sub-field A likely will not align with a Type tower from sub-field B. Further it seems you need to specify the sub-field of mathematics you are working in (e.g. Number Theory, Topology, Algebra, etc.) in order to capture the Definitions. Indeed, you have been saying something along the lines of "if we use Curry-Howard we can generate programs from LEAN and prove them correct" (likely a misquote on my part). I can tell you from experience that the Type hierarchy in LEAN and the Type hierarchy in Axiom's computer algebra suffer from this "misalignment" problem. Types for LEAN and Types for programming are different Type towers. This matters for both LEAN proofs and Axiom's algorithmic proofs. Curry-Howard is fine but the tools available to a mathematician and the tools available to a programmer differ in deep and subtle ways. Understanding Continuity conceptually is not the same as writing code that robustly captures the Definition or concept. Tim Daly [0] Andrei Bourchtein and Ludmila Bourchtein "CounterExamples: From Elementary Calculus To The Beginnings Of Analysis" https://www.amazon.com/CounterExamples-Elementary-Beginnings-Textbooks-Mathematics-ebook/dp/B07L6RJML3/ [1] https://www.amazon.com/s?k=counterexamples+in+analysis&crid=322LH8VEQGIJ5&sprefix=counterexamples%2Caps%2C146&ref=nb_sb_ss_p13n-expert-pd-ops-ranker_ci_hl-bn-left_1_15
