[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] QED Manifesto and Symbolic Algebra

From: Tim Daly
Subject: Re: [Axiom-developer] QED Manifesto and Symbolic Algebra
Date: Sun, 23 Dec 2018 23:44:59 -0500

I am rebuilding the Axiom compiler to support the algorihmic
proof technology.  It is a difficult problem and I still have much
to learn. However, I think that we need to connect the "proof"
side of computational mathematics with computer algebra
computational mathematics. After nearly 3 years taking courses
at CMU I think I see how it will succeed.

Whether *I* am capable of doing it is still an open question :-)


On 12/23/18, Eugene Surowitz <address@hidden> wrote:
> Tim:
> The notion of a "set of measure zero" could just
> be hiding the fact that they just don't know what it is ;)
> On to something less humorous:
> I am about to up grade my primary system to a MAC device
> with Windows 10 and Linux as alternate boots.
> This is part of a project I've been contemplating
> to try to develop a "dual" to AXIOM that would capture the
> experience of a "developer" who tries to build a system
> from scratch.  "Build" means taking the algebra code
> and compiling each component, one by one, until a full
> AXIOM system has achieved.
> Gene
> On 12/22/2018 5:17 PM, Tim Daly wrote:
>> 9. Too little care for rigor. It is notoriously easy to find "bugs" in
>> algorithms for symbolic
>> computation. To make matters worse, these errors are often regarded as
>> of no significance
>> by their authors, who plead that the result returned is true "except
>> on a set of measure
>> zero", without explicitly naming the set involved. The careful
>> determination, nay, even
>> proof, of precisely which conditions under which a result is true is
>> essential for building
>> the structure of mathematics so that one can depend on it. The QED
>> system will support
>> the development of symbolic algebra programs in which formal proofs of
>> correctness of
>> derivations are provided, along with the precise statement of
>> conditions under which the
>> results are true.
>> _______________________________________________
>> Axiom-developer mailing list
>> address@hidden

reply via email to

[Prev in Thread] Current Thread [Next in Thread]