[Top][All Lists]

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

Re: [Axiom-developer] Competing on "features" is for game programmers, n

From: Eugene Surowitz
Subject: Re: [Axiom-developer] Competing on "features" is for game programmers, not mathematicians
Date: Wed, 5 Jun 2019 11:38:27 -0400
User-agent: Mozilla/5.0 (Windows NT 5.1; rv:52.0) Gecko/20100101 Thunderbird/52.9.1

An amusing anecdote about proofs can be found in
"My Brain Is Open" by Bruce Schechter; the subtitle is
'The Mathematical Journeys of Paul Erdos'.

At the bottom of p.20 Erdos asks Andrew Vazsonyi
how many proofs of the Pythagorean theorem did he know.
Vazsonyi's answer was that he only knew one.
Erdos claimed to know 37.

A proven theorem is an invariant object.

Long lived and stable are different notions
more applicable to computer programs and systems
as you rightly point out.

Cheers, Gene

On 6/1/2019 7:00 AM, Tim Daly wrote:
I have an active discussion on Zulip / Lean (the general/syntax thread)

The issue is "long term stability".

Axiom code from the last century still compiles and gives the same answers.
Latex code from the last century still compiles and gives the same document.

I need to be able to write Definitions, Lemmas, and a Proof that will machine
check correctly at the "30 year horizon". It does me no good to use Lean to
prove Axiom's GCD algorithm if the proof fails next week.

Lisp had this problem and it was essentially solved with a standards effort
to create common lisp.

It does me no good to have a proof system where the tactics can change,
the syntax can change, and the kernel is unstable. I can't do long-term,
"30 year horizon" computational mathematics on that basis.

I think someone should raise the "common core proof standard effort"
so that all of the systems could import / export "raw" proofs (at a
minimum). Or at least a common core for systems using equivalent
logic rules.

It is reasonable to assume that a "proof" is a long-lived object and
that computational mathematical results are "stable".

Competing on "features" is for game programmers, not mathematicians.


Axiom-developer mailing list

reply via email to

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