Clarification of Skepticism

[Wolfgang Windsteiger]

Dear colleagues,

my advisor Bruno Buchberger uses to call it the "hot phase" vs the "cool 
phase" in mathematics.

The hot phase phase is where you use your imagination, draw weird 
sketches, use your intuition, draw analogies from other known areas, 
maybe even led by desires, come up with some conjectures, etc. etc. I 
think these are Harvey's "major intellectual JUMPS".

The cool phase is later when you have to strictly prove the things that 
emerged during the hot phase. These proofs should not be led by desires, 
probably keep imagination and intuition at a minimum. They should 
strictly follow the rules of logic in order not to miss corner cases, 
neglect side conditions, etc. etc. the usual minor or major flaws in 
mathematical proofs that all of us know. I think these are Harvey's 
"minor intellectual JUMPS".

Technology as such can help in both phases, probably, but the kind of 
technology for the two phases might be quite diverse. I see the 
important role of proof technology (automated/interactive) that was 
defended by some writers earlier mostly in the cool phase. And there it 
might be a useful tool even for those that do the hot phase with pencil 
and paper.

Ciao,
WW.

On 02.03.21 02:56, Harvey Friedman wrote:
> I think I need to clarify my Skepticism.
> 
> Serious mathematics generally involves major intellectual JUMPS. I see
> no evidence that these JUMPS can be simulated by any proof
> technologies.
> 
> At the core there are normally major intellectual jumps that do not
> seem to fit into possibilities in manageable sized spaces, or are
> amenable to reinforcement techniques and so forth.
> 
> HOWEVER, I do believe that serious mathematics also involves keeping
> things straight, and also MINOR intellectual JUMPS. But bookkeeping
> and minor intellectual jumps can be the sorts of things that are
> amenable to technology. I understand that several FOM writers like to
> use technology for minor intellectual jumps and management. But the
> incentive to do so without the prospect of it coming close to
> affecting Major Intellectual Jumps, doesn't seem to be there - unless
> you are already invested in some ways.
> 
> My work usually involves several major intellectual jumps, more minor
> intellectual jumps, and a fair amount of management. Whereas I can
> imagine some use of technology for the minor intellectual jumps, and
> the management, I do not imagine that for the several major
> intellectual jumps. And many of those major intellectual jumps, aside
> from POWERFUL MATHEMATICAL IMAGERY AND CREATIVE IMAGINATION, involve
> PHILOSOPHICAL REFLECTION, EXPERIENCED JUDGMENT CALLS, and DISCOVERIES
> OF NEW KINDS OF MATHEMATICAL STATEMENTS RESULTING FROM DECADES OF
> CONSTANT REFINEMENTS AND EXPERIMENTATION.
> 
> The minor intellectual jumps and the management, are so trivial in
> comparison, that I barely even notice them.
> 
> Now some of my projects - mostly unfinished - explicitly involve the
> analysis of a large but feasible set of finite structures. Obviously,
> technology can be crucial in such a context because the objects can be
> systematically explored by the technology in ways that are not
> feasible by the human brain. As a notable example, my proposals for
> the use of technology to search certain finite spaces which confirm
> the consistency of large cardinal hypotheses. But this is a
> specialized and unusual use of technology and not really proof
> assistants.
> 
> As you can see from earlier postings, I got interested in where the
> intellectual JUMPS become inaccessible to proof assistants. So I went
> into toy situations where the challenges are in a comparatively pure
> form. To take a ridiculously extreme case, look at the JUMP needed to
> go from ZFC to FLT. Is there anybody here on FOM that thinks that by
> 2100 one will be able to make that JUMP, from ZFC with exp to a proof
> of FLT in ZFC?
> 
> 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.
> 
> Harvey Friedman
> 

-- 
Assoc.Univ.-Prof. DI Dr. Wolfgang Windsteiger
RISC Institute / JKU Linz
Castle Hagenberg, 4232 Hagenberg i.M., Austria
Phone: +43 732 2468-9960
http://www.risc.jku.at/home/wwindste/
PGP: find the public key on my homepage