-
Mathematical Proof Between Generations
Authors:
Jonas Bayer,
Christoph Benzmüller,
Kevin Buzzard,
Marco David,
Leslie Lamport,
Yuri Matiyasevich,
Lawrence Paulson,
Dierk Schleicher,
Benedikt Stock,
Efim Zelmanov
Abstract:
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time th…
▽ More
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time this has been a topic for experts in specialized communities. However, mathematical proofs have become increasingly sophisticated, stretching the boundaries of what is humanly comprehensible, so that leading mathematicians have asked for formal verification of their proofs. At the same time, major theorems in mathematics have recently been computer-verified by people from outside of these communities, even by beginning students. This article investigates the gap between the different definitions of a proof and possibilities to build bridges. It is written as a polemic or a collage by different members of the communities in mathematics and computer science at different stages of their careers, challenging well-known preconceptions and exploring new perspectives.
△ Less
Submitted 8 July, 2022;
originally announced July 2022.
-
Longitudinal modeling of MS patient trajectories improves predictions of disability progression
Authors:
Edward De Brouwer,
Thijs Becker,
Yves Moreau,
Eva Kubala Havrdova,
Maria Trojano,
Sara Eichau,
Serkan Ozakbas,
Marco Onofrj,
Pierre Grammond,
Jens Kuhle,
Ludwig Kappos,
Patrizia Sola,
Elisabetta Cartechini,
Jeannette Lechner-Scott,
Raed Alroughani,
Oliver Gerlach,
Tomas Kalincik,
Franco Granella,
Francois GrandMaison,
Roberto Bergamaschi,
Maria Jose Sa,
Bart Van Wijmeersch,
Aysun Soysal,
Jose Luis Sanchez-Menoyo,
Claudio Solaro
, et al. (16 additional authors not shown)
Abstract:
Research in Multiple Sclerosis (MS) has recently focused on extracting knowledge from real-world clinical data sources. This type of data is more abundant than data produced during clinical trials and potentially more informative about real-world clinical practice. However, this comes at the cost of less curated and controlled data sets. In this work, we address the task of optimally extracting in…
▽ More
Research in Multiple Sclerosis (MS) has recently focused on extracting knowledge from real-world clinical data sources. This type of data is more abundant than data produced during clinical trials and potentially more informative about real-world clinical practice. However, this comes at the cost of less curated and controlled data sets. In this work, we address the task of optimally extracting information from longitudinal patient data in the real-world setting with a special focus on the sporadic sampling problem. Using the MSBase registry, we show that with machine learning methods suited for patient trajectories modeling, such as recurrent neural networks and tensor factorization, we can predict disability progression of patients in a two-year horizon with an ROC-AUC of 0.86, which represents a 33% decrease in the ranking pair error (1-AUC) compared to reference methods using static clinical features. Compared to the models available in the literature, this work uses the most complete patient history for MS disease progression prediction.
△ Less
Submitted 9 November, 2020;
originally announced November 2020.
-
Formalising perfectoid spaces
Authors:
Kevin Buzzard,
Johan Commelin,
Patrick Massot
Abstract:
Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover. This experiment confirms that a proof assistant can handle complexity in that direction, which is rather different from formalising a long proof about simple ob…
▽ More
Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover. This experiment confirms that a proof assistant can handle complexity in that direction, which is rather different from formalising a long proof about simple objects. It also confirms that mathematicians with no computer science training can become proficient users of a proof assistant in a relatively short period of time. Finally, we observe that formalising a piece of mathematics that is a trending topic boosts the visibility of proof assistants amongst pure mathematicians.
△ Less
Submitted 28 May, 2020; v1 submitted 27 October, 2019;
originally announced October 2019.
