"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 the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to fricas-devel+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/c24e770a-0447-4286-8c3e-326b7ab20528n%40googlegroups.com.
