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=3114 Tim Daly On Thu, Jan 8, 2026 at 8:48 AM 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 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 > > -- 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 email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/CAJn5L%3DKKFNeFjaMb136OiXu1a86%2BHU2XxPymKTSLTpVE4jc1jw%40mail.gmail.com.
