Re: Types capturing Definitions

--00000000000036e9440647e16f09
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Geoffrey Hinton was asked the question "How can you use AI to generate new
knowledge?".

I think his reply is relevant to the discussion. Perhaps capturing what
experts know now
is not the path to a generally intelligent AI mathematician. It might be
that the failing proofs
are actually the path to a better mathematician with new knowledge.
https://youtu.be/UccvsYEp9yc?t=3D3114

Tim Daly



On Thu, Jan 8, 2026 at 8:48=E2=80=AFAM Tim Daly <[email protected]> wrote:

> 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 thinki=
ng
> about ways to capture Types. It seems to me that Types are most useful wh=
en
> 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 tha=
t
> 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-Ma=
thematics-ebook/dp/B07L6RJML3/
>
> [1]
> https://www.amazon.com/s?k=3Dcounterexamples+in+analysis&crid=3D322LH8VEQ=
GIJ5&sprefix=3Dcounterexamples%2Caps%2C146&ref=3Dnb_sb_ss_p13n-expert-pd-op=
s-ranker_ci_hl-bn-left_1_15
>
>

--=20
You received this message because you are subscribed to the Google Groups "=
FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to [email protected].
To view this discussion visit https://groups.google.com/d/msgid/fricas-deve=
l/CAJn5L%3DKKFNeFjaMb136OiXu1a86%2BHU2XxPymKTSLTpVE4jc1jw%40mail.gmail.com.

--00000000000036e9440647e16f09
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>Geoffrey Hinton was asked the question &quot;How can =
you use AI to generate new knowledge?&quot;.</div><div><br></div><div>I thi=
nk his reply is relevant to the discussion. Perhaps capturing what experts =
know now</div><div>is not the path to a generally intelligent AI mathematic=
ian. It might be that the failing proofs</div><div>are actually the path to=
 a better mathematician with new knowledge.</div><div><a href=3D"https://yo=
utu.be/UccvsYEp9yc?t=3D3114">https://youtu.be/UccvsYEp9yc?t=3D3114</a></div=
><div><br></div><div>Tim Daly</div><div><br></div><div><br></div></div><br>=
<div class=3D"gmail_quote gmail_quote_container"><div dir=3D"ltr" class=3D"=
gmail_attr">On Thu, Jan 8, 2026 at 8:48=E2=80=AFAM Tim Daly &lt;<a href=3D"=
mailto:[email protected]">[email protected]</a>&gt; wrote:<br></div><bloc=
kquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:=
1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>I will b=
e following your work at <a href=3D"http://axiommath.ai" target=3D"_blank">=
http://axiommath.ai</a> closely. Since I&#39;ve been working</div><div>on A=
xiom (computer algebra) since the 1980s I have opinions :-)</div><div><br><=
/div><div>The connection betwen Types and mathematical Definitions is worth=
 capturing.</div><div><br></div><div>While trying to merge Axiom and LEAN I=
 spent a fair amount of time thinking</div><div>about ways to capture Types=
. It seems to me that Types are most useful when</div><div>they are organiz=
ed to support Definitions. For example, the type Continuous captures</div><=
div><span><span>that a function is continuous at
 a point if the limit as you approach that point equals the=C2=A0</span></s=
pan></div><div><span><span>actual=20
function&#39;s value at that point, with the limit existing and being the=
=20
same from both sides.</span></span></div><div><span><span><br></span></span=
></div><div><span><span>Of course, that assumes a Type capturing the defini=
tion of Limit, etc.</span></span></div><div><span><span><br></span></span><=
/div><div><span><span>This attempt at capturing Definitions as Types was th=
e basis of the SANE Axiom effort.</span></span></div><div><span><span><br><=
/span></span></div><div><span><span>From my continuous (pun intended) scrat=
ching at the problem I found whole textbooks [0][1]</span></span></div><div=
><span><span>that undermine any Type based on a definition. The whole effor=
t bogged down in so much</span></span></div><div><span><span>complexity I g=
ave up. To contruct a &quot;correct&quot; Type tower in any sub-field you n=
eed to be an</span></span></div><div><span><span>expert in that sub-field. =
Unfortunately the constructed Type tower in sub-field A likely will</span><=
/span></div><div><span><span>not align with a Type tower from sub-field B. =
<br></span></span></div><div><span><span><br></span></span></div><div><span=
><span>Further it seems you need to specify the sub-field of mathematics yo=
u are working in</span></span></div><div><span><span>(e.g. Number Theory, T=
opology, Algebra, etc.) in order to capture the Definitions.</span></span><=
/div><div><span><span><br></span></span></div><div><span><span>Indeed, you =
have been saying something along the lines of &quot;if we use Curry-Howard<=
/span></span></div><div><span><span>we can generate programs from LEAN and =
prove them correct&quot; (likely a misquote on my part).</span></span></div=
><div><span><span>I can tell you from experience that the Type hierarchy in=
 LEAN and the Type hierarchy in</span></span></div><div><span><span>Axiom&#=
39;s computer algebra suffer from this &quot;misalignment&quot; problem. Ty=
pes for LEAN and</span></span></div><div><span><span>Types for programming =
are different Type towers. This matters for both LEAN proofs</span></span><=
/div><div><span><span>and Axiom&#39;s algorithmic proofs.</span></span></di=
v><div><span><span><br></span></span></div><div><span><span>Curry-Howard is=
 fine but the tools available to a mathematician and the tools available</s=
pan></span></div><div><span><span>to a programmer differ in deep and subtle=
 ways. Understanding Continuity conceptually</span></span></div><div><span>=
<span>is not the same as writing code that robustly captures the Definition=
 or concept.</span></span></div><div><span><span><br></span></span></div><d=
iv><span><span>Tim Daly</span></span></div><div><span><span><br></span></sp=
an></div><div><span><span>[0] </span></span>Andrei Bourchtein and Ludmila B=
ourchtein &quot;CounterExamples: From Elementary Calculus To The Beginnings=
 Of Analysis&quot;</div><div><a href=3D"https://www.amazon.com/CounterExamp=
les-Elementary-Beginnings-Textbooks-Mathematics-ebook/dp/B07L6RJML3/" targe=
t=3D"_blank">https://www.amazon.com/CounterExamples-Elementary-Beginnings-T=
extbooks-Mathematics-ebook/dp/B07L6RJML3/</a></div><div><br></div><div>[1]
=20
<a href=3D"https://www.amazon.com/s?k=3Dcounterexamples+in+analysis&amp;cri=
d=3D322LH8VEQGIJ5&amp;sprefix=3Dcounterexamples%2Caps%2C146&amp;ref=3Dnb_sb=
_ss_p13n-expert-pd-ops-ranker_ci_hl-bn-left_1_15" target=3D"_blank">https:/=
/www.amazon.com/s?k=3Dcounterexamples+in+analysis&amp;crid=3D322LH8VEQGIJ5&=
amp;sprefix=3Dcounterexamples%2Caps%2C146&amp;ref=3Dnb_sb_ss_p13n-expert-pd=
-ops-ranker_ci_hl-bn-left_1_15</a></div><br></div>
</blockquote></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;FriCAS - computer algebra system&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:[email protected]">fricas=
[email protected]</a>.<br />
To view this discussion visit <a href=3D"https://groups.google.com/d/msgid/=
fricas-devel/CAJn5L%3DKKFNeFjaMb136OiXu1a86%2BHU2XxPymKTSLTpVE4jc1jw%40mail=
.gmail.com?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.co=
m/d/msgid/fricas-devel/CAJn5L%3DKKFNeFjaMb136OiXu1a86%2BHU2XxPymKTSLTpVE4jc=
1jw%40mail.gmail.com</a>.<br />

--00000000000036e9440647e16f09--