By Nicolas Behr
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.
By Dimitry Gurevich
By Vincent Rivasseau , Léonard Ferdinand
By James Propp
By Paul-André Melliès
By Alexandros Singh
By Sergey Yurkevich
By Cyril Banderier
By Stéphane Gaubert
By Vincel Hoang Ngoc Minh
By Lionel Pournin
By Claudio Dappiaggi
By Alexander Strohmaier
By Hans Lindblad
By Misha Gromov
By Olivier Benoist
By Viviane Pons
