Towards the Formal Certification of a Mathematical Encyclopedia on the Web

Description

Niveau: Supérieur, Doctorat, Bac+8
Towards the Formal Certification of a Mathematical Encyclopedia on the Web Frederic Chyzak and Assia Mahboubi? Keywords Coq, formal proofs, computer algebra, hypergeometric sums, creative telescop- ing, Apery constant. Context The last decade has seen the development of large bodies of online digitalized mathematical knowledge. The Dynamic Dictionary of Mathematical Functions (DDMF) [DDM] is one of these web sites, on which properties of the math- ematical functions are obtained interactively, by dynamically executing some computer-algebra libraries, then displaying them. This project is targeted to readers who are not experts in computer algebra, and sometimes express doubts about the displayed equations. One of its specificities is that it provides them with some guarantee about the correctness of the symbolic calculations per- formed to obtained the requested answer: certificates are obtained by a manual instrumentation of the symbolic code executed, and they are displayed on the web page as a sketch of correctness proof, in natural language. Proof assistants are another kind of mathematical software, which are de- voted to helping mathematicians to check the correctness of the proofs they invent. This machine-check process is often considered as the highest possi- ble correctness guarantee that can be obtained for proofs, specially when they are too tedious to be reliably verified by a human being. This guarantee how- ever has a cost: in the current state of the art, describing mathematical proofs in a proof assistant is still a long and demanding effort, requiring expertise in the domain of mathematics formalization.

• section devoted


• apery's proof


• formal proofs—the


• hypergeometric sums


• mathematical functions


• possi- ble correctness


• such formal


• proof assis


• proof assistant

Sujets

• Harrison
• Gonthier
• Paul Gottlieb Nipkow
• Johannes Kepler

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 18
• Langue: English

Extrait

Towards the Formal Certification of a Mathematical Encyclopedia on the Web

∗ Fr´ed´ericChyzakandAssiaMahboubi

Keywords Coq, formal proofs, computer algebra, hypergeometric sums, creative telescop- ing,Ap´eryconstant.

Context The last decade has seen the development of large bodies of online digitalized mathematical knowledge.The Dynamic Dictionary of Mathematical Functions (DDMF) [DDM] is one of these web sites, on which properties of the math- ematical functions are obtained interactively, by dynamically executing some computer-algebra libraries, then displaying them.This project is targeted to readers who are not experts in computer algebra, and sometimes express doubts about the displayed equations.One of its specificities is that it provides them with some guarantee about the correctness of the symbolic calculations per- formed to obtained the requested answer:certificates are obtained by a manual instrumentation of the symbolic code executed, and they are displayed on the web page as a sketch of correctness proof, in natural language. Proof assistants are another kind of mathematical software, which are de- voted to helping mathematicians to check the correctness of the proofs they invent. Thismachine-check process is often considered as the highest possi- ble correctness guarantee that can be obtained for proofs, specially when they are too tedious to be reliably verified by a human being.This guarantee how- ever has a cost:in the current state of the art, describing mathematical proofs in a proof assistant is still a long and demanding effort, requiring expertise in the domain of mathematics formalization.Recent successful formalizations + [Gon08, HHM10] have started changing this situation.It hence seems relevant to question the feasibility of checking realistic mathematical software, using proofs-assistant software. ∗ E-mail addresses:[e-mail]

1