Proof Technology and Ideas

[Ignacio Añón]

Harvey Friedman wrote:

" I would like to see an understandable discussion, without JARGON, of
what kind of JUMPS can already be made or are in the cards to be made
by proof technology."

The fact that there might exist the possibility of controlling, by
given upper bounds, any polynomial with integer coefficients, whose
solution in nonnegative integers is neither refutable nor provable in
PA, is so powerful, and might have such technological consequences,
that it is even a little frightening...

It is frustrating that almost no one in the FOM community, knows what
the LDPC conjecture is, or that lately, minds like Edward Witten, have
been interested in that embrionary science we call "information
technology".

Without conflating the use of technology as an aid to discovery, with
proof assistants as a standard of rigour, there is, nevertheless, it
seems to me, an important thing missing in the discussion: historical
sense...

We are giving birth to certain ideas, that will manifest in technology
and or math, which will leave the discussion about the relevance of
proof assistants, and about the use of technology to enhance
discovery, way behind.

No one loves the original, subtle work done by people like Turing,
Kleene, Godel, Von Neumann and others, laying the foundations of what
we conceive as a rigorous notion of "computable function", as I do.
And yet, all this work, was utterly irrelevant, for the conception of
the modern semi-conductor...

The "Jump" that the invention of the transistor and the semi-conductor
represented, came from a realm of ideas, completely foreign to Men
like Turing, Kleene and Von Neumann...

The manichean dichotomy between "technology", and mathematical
intelectual conceptions, is illusory: there is trivial, academic,
work, done in any field: proof assistants, FOM, information theory,
and digital technology, are no exception...

Solid state physics, is based on a subtle, anonymous, non academic,
cultural, creative idea: out of it came the modern digital era, and
its technology. There are certain ideas, within FOM, that are as
subtle, and powerful, as it. Among them, is the possibility,
predicated by Godel in his later years, of generalizing Stone-type
Boolean representations, to larger and larger areas of foundations...

In proof assistants, it is difficult to find any realm of ideas as
interesting as those of solid state physics, or the Godel
Stone-insight...

This insight, comes out of an historical tradition, begun by the early
pioneers of the first scientific revolution. For them, the mechanistic
dream of controlling the world via technology, and mathematical ideas,
were the same thing(Descartes, Leibniz...)

A tiny bit of historical sense, is enough to see this...