Orateur
Description
This talk will present the ”coreact.wiki” initiative, which aims to develop a novel form of wiki engine that will couple a database of human-readable mathematical knowledge with a database containing machine-readable and -executable representations of this knowledge in proof assistants such as Coq. For the concrete example of analytic combinatorics à la Flajolet and Sedgewick, I will provide an overview of the types of statements that can be efficiently formalized in Coq at present and in the near future, and how we plan to provide an interactive web-based interface to the ”coreact.wiki” platform based upon jsCoq to permit computations and formal proofs in a user-friendly fashion. Time permitting, I will also sketch the possibility of extracting prototypical reference algorithms from formalized categorical statements in Coq via the use of SMT solvers.
