Jamais avant l’arrivée des ordinateurs on n’aurait imaginé que certains écrivains abandonneraient le crayon et le papier. Des logiciels de traitement de texte évolués rendent depuis quelques décennies la chose possible.
Ce type de transition ne concerne encore que peu de mathématiciens mais cela n’est pas nécessairement une fatalité. On peut espérer produire un logiciel dont l’utilisation serait aussi simple que de faire une démonstration sur papier.
Si c’était le cas, beaucoup de mathématiciens choisiraient alors de s’en servir.
En effet, l’utilisation de la technologie apporte d’autres avantages au passage tels qu’une gestion facilitée des versions au fur et à mesure des progrès, une aide à la rédaction, mais aussi l’avantage évident que les démonstrations auront entièrement été vérifiées et ne comporteront donc pas d’inexactitudes ou d’hypothèses implicites.
Il y a quelques années, Tim Gowers, médaillé Fields, a lancé sur son blog le défi d’une démonstration mathématique réalisée en collaboration avec de nombreux mathématiciens, via le web \cite{Gowers_2009}.
Ce projet, qui a aussi reçu le soutien de Terence Tao, un autre médaillé Fields, fut un succès et la démonstration fut publiée \cite{Polymath_2012}.
Parmi les participants, des chercheurs mais pas seulement \cite{Cranshaw_2011}. Si l’on souhaite reproduire l’expérience à une échelle plus large, en ouvrant les portes de la démonstration collaborative à davantage d’amateurs, des outils plus sophistiqués seront nécessaires et on peut imaginer les baser sur un assistant de preuve accessible tel que nous souhaitons aider à construire.