Recently, Mike Freedman, a Fields medalist, formalized his paper in LEAN. He told me there was a bad taste in his mouth because when they published the paper the results were checked with a computer algebra system. For mathematicians this is like blasphamy to have something like an unverified computer algebra system check, just like your result is not real, because you needed a computer algebra system. People believe there are many bugs. But, [using Lean] we could check again the many results. --- https://youtu.be/saZUBqdduTY?t=1433
On Tue, Jul 15, 2025 at 6:55 AM Tim Daly <[email protected]> wrote: > > "Ah, but a man's reach should exceed his grasp, Or what's a heaven for?" > -- Robert Browning > > Obviously my SANE (synomym for rational, coherent, judicious, sound) > version of computational mathematics was beyond my reach but the idea > of having a formally provable computer algebra system is possible. > > Computer algebra based on dependent types is possible. > A Proof system that formally proves computer algebra algorithms is > possible. > > Merging computer algebra and proof systems is not only possible > it is the required step forward from the last century's efforts. > > Computational Mathematics (computer algebra plus proof) is possible. > > > Algebraic Reasoning is fundamental to modern mathematics. We calculate > with abstract structures the same way we calculate with numbers; for > example, we take sums, products, powers, and limits of structures just > as we take sums, products, powers, and limits of numbers. Then, in the > same breath, we talk about elements of those structures and operations > on those elements. To formalize this kind of reasoning, we need a > language in which types and structures are first-class objects, and we > need tools that can interpret ambiguous notation and fill in the > information that is left implicit in informal mathematics. There is no > way around using dependent type theory for all that. > --- Jeremy Avigad, CMU > > "Lean: Machine-Checked Mathematics And Verified Programming" > --- https://youtu.be/saZUBqdduTY?t=353 > > From the beginning Lean was developed on dependent type theory. We were > studying many different approaches and we wanted a system that would > be great for math. Our first user was Jeremy Avigad. He is a > mathematician. He made this point over and over again that in abstract > math you need to manipulate many objects like Groups, Rings, Fields. > They all should be first-class citizens. You should manipulate them as > objects in your language and there is no other way around. Of course, > people will say "Oh, yeah, we can use this crazy coding" but we do not > want our users to be distracted with coding tricks. People who say we > can use fancy coding tricks are the same people who say "You can > program anything in a Turing machine". Who is going to do that? > Nobody. You want to work at the right level of abstraction. We want to > enable our users to focus on the math not on encoding tricks. > --- Leonardo de Moura, Author of LEAN. > > -- > You received this message because you are subscribed to a topic in the > Google Groups "FriCAS - computer algebra system" group. > To unsubscribe from this topic, visit > https://groups.google.com/d/topic/fricas-devel/I21L2RZFXUs/unsubscribe. > To unsubscribe from this group and all its topics, send an email to > [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/fricas-devel/c24e770a-0447-4286-8c3e-326b7ab20528n%40googlegroups.com > <https://groups.google.com/d/msgid/fricas-devel/c24e770a-0447-4286-8c3e-326b7ab20528n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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%3DLK%3D-guABtRa7qu01TMWFRjAgLBeRbeotmTYqNCgWn1fg%40mail.gmail.com.
