| Register
\(\newcommand{\Cat}{{\rm Cat}} \) \(\newcommand{\A}{\mathcal A} \) \(\newcommand{\freestar}{ \framebox[7pt]{$\star$} }\)

1. General questions

Here we collect general questions about aspects of computer-assisted proofs

    1. Are Computer-assisted proofs real proofs?


      Add remark

      Problem 1.1.

      [K. Buzzard] Are computer-assisted proofs always real proofs when proprietary software and/or hardware is involved that is not accessible to all readers/reviewers?
          Follow-up comments/questions: Is it preferable to use pseudo-code rather than a programming language? Can everyone access hardware to perform the computations involved?-Are such proofs reproducable? Does this have impacts on the review process? Does one have to submit the entire virtual machine? How should one disentangle the human and computer-assisted part? Should a computer-assisted part be computer-verifiable?

        • What is the right metric to determine computability?


          Add remark

          Problem 1.2.

          [Y. T. Hou] In problems where mathematical analysis precedes a computer assisted step: How can we ensure that the formulation of problem is correctly posed so that computability and non-computability of a problem can be determined?
              Follow-up comments/questions: What is the right metric (and in case of PDEs also the function space) to determine computability and non-computability?-A problem might be computable in one class of problems but computable in another class. (reference to SCI-hierarchy in the morning talk by Bastounis and Colbrook!)

            • How should limitations in technology for conjectures/discoveries be adressed?


              Add remark

              Problem 1.3.

              [P. Deift] Can we uncover quantitative properties such as periodicity from numerical methods for PDEs? - In particular for integrable systems. Does (or should) a correct notion of computability depend on the hardware available at the current state of time? - How should we present work with highly experimental evidence?
                  Follow-up comments/questions: Should this idea rather apply to conjectures heuristics? Should numerical methods be held more accountable for a very careful convergence study?- As they might turn out to be wrong later on.

                • Computer-assisted proof of Mochizuk’s work on the ABC conjecture!


                  Add remark

                  Problem 1.4.

                  [J. Lagarias] Can one set up a machine-verifiable proof of the work by Mochizuki trying to proof the ABC conjecture?
                      Follow-up comments/questions: How should one document mathematics? - This may not be possible at the moment.

                    • Make computer-assisted proofs and software more accessible to math community!


                      Add remark

                      Problem 1.5.

                      [J. Dahne] What do mathematicians find difficult about working with computer-assistance in Mathematics? How can software be improved from the view of users to ?
                          Follow-up comments/questions: How to standardise computer-assisted proofs. What about eigenvalue problems?- Should there exist standardised software for computer-assisted proofs related to eigenvalue problems. How can one "trust" mathematical software?


                        • Add remark

                          Problem 1.6.

                          [J. Dahne] Make computer-assisted proofs and software more accessible to math community!
                              Follow-up comments/questions: How to standardise computer-assisted proofs. What about eigenvalue problems?- Should there exist standardised software for computer-assisted proofs related to eigenvalue problems. How can one "trust" mathematical software?

                            • Define Space complexity!


                              Add remark

                              Problem 1.7.

                              [J. Lagarias] Does there exist a notion of space complexity?

                                • How to use AI for computer-assisted proofs?


                                  Add remark

                                  Problem 1.8.

                                  [A. Hansen] How to use AI for computer-assisted proofs?

                                    • Validating numerics for analysis


                                      Add remark

                                      Problem 1.9.

                                      [F. Bernhard] How can we produce rigorous numerics with an emphasis on questions arising in mathematical analysis?

                                          Cite this as: AimPL: Computational mathematics in computer assisted proofs , available at http://aimpl.org/compproofs.