| Joe Corneli |
| Mon 18 Feb 2019, 14:00 - 15:00 |
| IF 4.31/4.33 |
If you have a question about this talk, please contact: Allison Kruk (v1atayl6)
Title
Design Requirements for a Formal Abstracts Service
Abstract
The mathematician Tom Hales is leading a project to create a substantial collection of statements of published mathematical theorems, together with the relevant definitions, which will be represented in both a computer and human readable way. Strikingly, the proofs of these theorems will be omitted: Hales calls the elements of the collection "formal abstracts."
This talk will discuss design requirements for a future formal abstracts service from three points of view: theorem proving, computer algebra, and digital libraries. As a use case, we reexamine a problem in elementary differential equations that was previously addressed with Maple and PVS. We look at how to port the earlier Maple/PVS solution to the ecosystem that is developing around the Lean theorem prover, and discuss the potential role(s) of formal abstracts in a new solution.
We consider the relationship of the formal abstracts to proof automation, synergies with computer algebra systems, and various library features will need to be addressed in order for the project to "scale up."