Types as Definitions
4 views
Skip to first unread message
Tim Daly
Jan 8, 2026, 8:46:48 AMJan 8
to FriCAS - computer algebra system
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"
Reply all
Reply to author
Forward
0 new messages