Generation and presentation of formal mathematical documents (Q2760868)

The aim of this Ph.D. thesis is to explore the role that could play the computer mathematics field in the development of mathematics. Chapter 2 of the book presents a gentle introduction to type theoretical theorem proving, and argues that type theory could be a good candidate for the language devoted to encode the formal mathematical discourse. This chapter exposes, as concrete type theory, the calculus of inductive constructions, the system standing behind the Coq theorem prover. Chapter 3 investigates computations in theorem provers, with an application to automated theorem proving for certain classes of problems, on the basis of reflection method. Chapter 4 describes an implementation of a tool which presents formalized mathematical theories as interactive natural language mathematical documents. Chapter 5 demonstrates that theroem proving and computer algebra systems can be combined to get efficient albeit formal proofs. This demonstration is supported by a generator which automatically produces proofs of primality that are formally verifiable. The Pocklington's criterion for testing primality of numbers is used to produce the primality proofs. The final Chapter 6 presents the conclusions of this thesis, emphasizing the new proposed approach and the obtained results.