From ba041dc8cc2392c020af8c34166110c93c08cf52 Mon Sep 17 00:00:00 2001 From: Joe Corneli Date: Tue, 30 May 2017 19:04:21 +0100 Subject: [PATCH] say something about Ganesalingam and Gowers --- org/farm-2017.org | 81 ++++++++++++++++++++++++++++++++++++++----------------- org/farm-refs.bib | 61 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 117 insertions(+), 25 deletions(-) diff --git a/org/farm-2017.org b/org/farm-2017.org index d0e7b6d..94fefb4 100644 --- a/org/farm-2017.org +++ b/org/farm-2017.org @@ -433,7 +433,7 @@ it, without the need to bracket it off from the rest of the proof. [fn:2] http://metameso.org/ar/gowers-example.pdf. [fn:3] From Wikipedia: Formally, a hypergraph $H$ is a pair $H = (X,E)$ where $X$ is a set of elements called ``nodes'' or ``vertices'', and $E$ is a set of non-empty subsets of $X$ called ``hyperedges'' or ``edges''. (https://en.wikipedia.org/wiki/Hypergraph) -** <<3.2>> 3.2 A `quantum of progress' +** <<3.2>> 3.2 Searching for the `quantum of progress' There is a further issue here, which the =implements= certificate hints at. Just how does the person working through a proof attempt @@ -441,33 +441,41 @@ decide which step to take next? In another setting, Gowers provides some very helpful guidance. The Polymath project aimed to answer the question "is massively -collaborative mathematics possible?" This project was convened by -Gowers in XXXX[fn:: http://gowers.wordpress.com/is-massively-collaborative-mathematicspossible/] -and he developed 15 rules to address the "questions of procedure" -that he anticipated would arise in the project.[fn:: http://gowers.wordpress.com/questions-of-procedure/ ]] - -In particular, the rules emphasize that a good contribution represents a "quantum of -progress." Gowers progressively and carefully explicated the imperative to share comments that are "not fully thought out."[fn:UMEM] As our representation and reasoning strategy comes into focus, it is now clear that we are searching for such quanta! - -[fn:UMEM] Ursula Martin had commented ten years earlier, with regard to the emerging field of /experimental mathematics/ that the growth of experimentation requires the "development of community standards as to experimental methodology," emphasizing not only technical matters, but also "the early sharing of insights" (Martin, 1999). +collaborative mathematics possible?" This project was convened by +Gowers in 2009, and he developed 15 rules to address the "questions of procedure" +that he anticipated would arise in the project.[fn:: http://gowers.wordpress.com/questions-of-procedure/ ] The basic premise was that people would work together on a +shared blog to discuss a given mathematical problem in the open, +and jointly work out a solution.[fn:: Incidentally, the conclusion to the main motivating question was a tentative ``yes'' \cite{gowers2009massively}. New Polymath projects continue to be run to the present day. Four Minipolymath project (including our "MPM") have been convened in the same spirit.] + +Gowers carefully explicated the imperative to share comments that are +"not fully thought out."[fn:UMEM] A good contribution to the project +would comprise what he called a "quantum of progress." Continuing +with this metaphor, as the KRR strategy we are developing comes more +fully into focus, it should be clear that we need to better understand +the "fields" that generate these quanta! That is, in order to build a +functional representation of mathematical reasoning, we need to model +both what's there at any given step, and also how it evolves -- noting +that such evolution is generally heuristic. + +Here one can compare Gowers's work with Ganesalingam on a +``human-oriented theorem proving'' system \cite{Ganesalingam2016}. +First, we will comment that this work motivated the presentation of +GCP. However, Ganesalingam and Gowers's system was only able to solve +more straightforward "textbook" problems, in which the next step is +always more or less "obvious". Under the hood, there is a Logic of +Computable Functions (LCF) style inference system. + +[fn:UMEM] Ursula Martin had commented ten years earlier, with regard to the emerging field of "experimental mathematics," that the growth of experimentation requires the "development of community standards as to experimental methodology," emphasizing not only technical matters, but also "the early sharing of insights" \cite{martin1999computers}. * 4 APPLICATIONS Our latest efforts produce more detailed models of mathematical arguments. :JOE: -We need to model what's there and how it evolves, noting that -evolution is heuristic. One example Sussman gives of modelling "`how -to' as well as `what is'" \cite{sussman2005programming}, is a LISP -program that he wrote with Richard Stallman that can replicate the -process of analyzing a circuit \cite{sussman2011programming}. The -program explains /why/ it comes up with the answers it does. The "why -question" is perhaps even more important (and interesting) when -nontrivial ``creativity'' is involved in the reasoning process -\cite{gucklesberger2016addressing}. - -#+BEGIN_COMMENT -The program could take the wiring diagram of the circuit, calculate -the current at some point, and recapitulate the assumptions and rules -that led the program to its answer. -#+END_COMMENT +One example Sussman gives of modelling "`how to' as well as `what is'" +\cite{sussman2005programming} is a LISP program that he wrote with +Richard Stallman that can replicate the process of analyzing a circuit +\cite{sussman2011programming}. The program explains /why/ it comes up +with the answers it does. The "why question" is perhaps even more +important (and interesting) when nontrivial ``creativity'' is involved +in the reasoning process \cite{gucklesberger2016addressing}. ** <<4.1>> 4.1 Kinematics (IATC+CD) ** <<4.2>> 4.2 Dynamics (Lytinen's stuff with goals and scripts) @@ -520,6 +528,29 @@ Sperber & Mercier \cite{mercier2017enigma}. Even if we are not interacting directly with others, "appropriate inferential norms" are social constructions. Indeed, Minsky saw thought as inherently social. +Quite contrary to the sentiment conveyed by the +misattributed quote ``Mathematics is a game played according to +certain simple rules with meaningless marks on paper,'' David Hilbert, +an early and important proponent of mathematical formalism, emphasised +the role of intuition and experience, and discussed conjectural +thinking and the fallibility of mathematical reasoning +\cite{hilbert1992natur,corry1997origins}.[fn:thomae] + +[fn:thomae] The actual source of the quote appears to be Carl Johannes +Thomae, /Elementare Theorie der analytische Functionen einer complexen +Veraenderlichen/ (1898), p. 3: For the formalist, arithmetic is a game +with signs, which are called empty. That means they have no other +content (in the calculating game) than they are assigned by their +behaviour with respect to certain rules of combination (rules of the +game) It is worth noting that Thomae nevertheless continues on to +remark on the difference between arithmetic and chess, insofar as +``numbers can be related to concrete manifolds by means of simple +axioms.'' Cf. this discussion in the ``Foundations of Mathematics'' +mailing list: +https://www.cs.nyu.edu/pipermail/fom/2005-April/008889.html. + +* ON HOLD + ----- * 7 PART TWO In our planned next steps we plan to bring in explicit type-theoretic representations of mathematical objects within a service-oriented architecture. :onhold: diff --git a/org/farm-refs.bib b/org/farm-refs.bib index 96d6348..938b2b7 100644 --- a/org/farm-refs.bib +++ b/org/farm-refs.bib @@ -346,4 +346,65 @@ editor={Goel, Ashok and Jordanous, Anna and Pease, Alison and Jacob, Mikhail and booktitle={Proceedings of the Eighth International Conference on Computational Creativity, ICCC 2017}, year={2017}, url={http://computationalcreativity.net/iccc2017/ICCC_17_accepted_submissions/ICCC-17_paper_37.pdf} +} + +@inproceedings{martin1999computers, + title={Computers, reasoning and mathematical practice}, + author={Martin, U.}, + booktitle={{Computational} {Logic}: {Proceedings} of the {NATO} {Advanced} {Study} {Institute} on {Computational} {Logic}}, + pages={301--346}, + editor={Ulrich Berger and Helmut Schwichtenberg}, + year={1999}, + organization={Springer}, + note={Held in Marktoberdorf, Germany, July 29 – August 10, 1997.} +} + +@book{hilbert1992natur, + title={Natur und mathematisches Erkennen: Vorlesungen, gehalten 1919-1920 in G{\"o}ttingen}, + author={Hilbert, David}, + year={[1919] 1992}, + publisher={Birkh{\"a}user} +} + +@article{corry1997origins, + title={The origins of eternal truth in modern mathematics: {Hilbert} to {Bourbaki} and beyond}, + author={Corry, Leo}, + journal={Science in Context}, + volume={10}, + number={02}, + pages={253--296}, + year={1997}, + publisher={Cambridge Univ Press} +} + +@misc(gowers-massively, + author={Gowers, Timothy}, + title={Is massively collaborative mathematics possible?}, + howpublished={\url{http://gowers.wordpress.com/is-massively-collaborative-mathematics-possible/}}, + note = {Accessed: 2017-05-30} +) + + +@Article{Ganesalingam2016, +author="Ganesalingam, M. +and Gowers, W. T.", +title="A Fully Automatic Theorem Prover with Human-Style Output", +journal="Journal of Automated Reasoning", +year="2016", +pages="1--39", +abstract="This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians.", +issn="1573-0670", +doi="10.1007/s10817-016-9377-1", +url="http://dx.doi.org/10.1007/s10817-016-9377-1" +} + +@article{gowers2009massively, + title={Massively collaborative mathematics}, + author={Gowers, W.T. and Nielsen, M.}, + journal={Nature}, + volume={461}, + number={7266}, + pages={879--881}, + year={2009}, + publisher={Nature Publishing Group} } \ No newline at end of file -- 2.11.4.GIT