Re: QED Manifesto and Symbolic Algebra

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 :-)

Tim

On 12/23/18, Eugene Surowitz <[email protected]> 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
>> [email protected]
>> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>>
>