Je pense qu’il suggérait que le Frido, vu sa politique justement de tout démontrer, pourrait quasi être réécrit en Lean ou ce type d’assistant de preuve. Ça permettrait notamment de s’assurer qu’il n’y a pas d’erreurs, et de fournir une formalisation des preuves elles mêmes. Ça fait vaguement penser à la démarche de Knuth d’écrire son TeX book en TeX, la partie textuelle serait une documentation des preuves écrites dans une langue formelle.
Mais c’est un boulot énorme, encore plus que le Frido sans doute vu que l’assistant vient avec son lot de difficultés propres et qu’il est à peu près fini.
[^] # Re: Typos, erreurs et preuves
Posté par thoasm . En réponse à la dépêche Sortie du Frido pour les Matheux. Évalué à 5.
Je pense qu’il suggérait que le Frido, vu sa politique justement de tout démontrer, pourrait quasi être réécrit en Lean ou ce type d’assistant de preuve. Ça permettrait notamment de s’assurer qu’il n’y a pas d’erreurs, et de fournir une formalisation des preuves elles mêmes. Ça fait vaguement penser à la démarche de Knuth d’écrire son TeX book en TeX, la partie textuelle serait une documentation des preuves écrites dans une langue formelle.
Mais c’est un boulot énorme, encore plus que le Frido sans doute vu que l’assistant vient avec son lot de difficultés propres et qu’il est à peu près fini.