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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Tim Daly
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.

Tim

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Competing on "features" is for game programmers, not mathematicians

Tim Daly
Axiom has a "30 Year Horizon" project goal, looking to develop the
techniques and technology for reliable, proven computational
mathematics.

I'm trying to prove Axiom Sane (rational, judicious, sound, logical)
by constructing axioms and specifications for functions (actually,
only the GCD functions since I'm not gonna live long enough to do
much more :-) )

It is clearlly important to construct proofs that can be checked
at compile time, every time, to ensure that Axiom is still
mathematically sound despite changes.

Apparently this kind of "30 Year Horizon" stability isn't a project
goal for a lot of the systems.I find this suprising since Gentzen's
rules seem like a solid logic kernel you'd have to implement.

Robinson's resolution paper was in 1965 so proof technology is as
old as computer algebra (SAINT/SIN). After  50+ years, it seems
reasonable to think about standards.

Both of you have influence across both areas of computational
mathematics. Perhaps you can find consensus for at least the
beginnings of an effort to consider cooperation on a standard.

Tim




On 6/1/19, James Davenport <[hidden email]> wrote:

> Especially "non-upwards-compatible" features. There was a discussion at Big
> Proof 2019 about the fragility of Big Proofs, and indeed it was asked
> whether the Classification of Finite Simple Groups was still proved. I THINK
> the question was slightl tongue-in-cheek, but nevertheless it's a good
> question.
>
>
> James Davenport
> Hebron & Medlock Professor of Information Technology, University of Bath
> National Teaching Fellow 2014
> OpenMath Content Dictionary Editor
> Former Fulbright CyberSecurity Scholar (at New York University)
> Vice-President and Academy Chair, British Computer Society
> ________________________________
> From: Tim Daly <[hidden email]>
> Sent: 01 June 2019 12:00:03
> To: Jeremy Avigad; James Davenport; axiom-dev; [hidden email]
> Subject: Competing on "features" is for game programmers, not
> mathematicians
>
> 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.
>
> Tim
>

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Competing on "features" is for game programmers, not mathematicians

Eugene Surowtz
In reply to this post by Tim Daly
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.
>
> Tim
>
> _______________________________________________
> Axiom-developer mailing list
> [hidden email]
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer