[FOM] Proof and open source software

[Jay Halcomb]

Regarding the open source software debate and also the questions
concerning 'what is a proof?' (formalized or informal, verified
by humans or by software), this AMS Notices Opinion is pertinent
http://www.ams.org/notices/200710/tx071001279p.pdf

Selections:

'I think we need a symbolic standard to make computer
manipulations easier to document and verify.And with all due
respect to the free market, perhaps we should not be dependent
on commercial software here. An open  source project could,
perhaps, find better answers to the obvious problems such  as
availability, bugs, backward compatibility, platform
independence, standard  libraries, etc. One can learn from the
success of TEX and more specialized software like Macaulay. I do
hope that funding agencies are looking into this.' -Andrei
Okounkov, 2006 Fields medalist
...

'There is a proof in the article by Campbell et al. in The Atlas
of Finite Groups-Ten Years On (1998) that describes how many
separate software packages were "easily used" to deduce various
mathematical facts-no code is given, and some of the programs
are proprietary software that runs only on hardware many years
out of date. Such proofs may become increasingly common in
mathematics if something isn't done to reverse this trend.'

'..suppose now Jane [an imaginary mathematician] says a theorem
is true based partly on the results of software. The closest we
can reasonably hope to get to a rigorous proof (without new
ideas) is the open inspection and ability to use all the
computer code on which the result depends. If the program is
proprietary, this is not possible.To quote J. Neubüser, "with
this situation two of the most basic rules of conduct in
mathematics are violated: In mathematics information is passed
on free of charge and everything is laid open for checking." '

Cheers,
Jay

Jay Halcomb
H&S Information Systems
http://hsinfosystems.com