Il y a plusieurs manières de gérer "l’habitude", soit tu utilises un théorème classique et dans ce cas une fois démontré il est dans une bibliothèque prêt à être utilisé, en principe ...
Ultimement et avec une bonne connaissance de l’écosystème, le côté "nouveau" ou "inhabituel" pourrait se déduire potentiellement du non emploi de ces techniques ou théorèmes pour démontrer des choses nouvelles. À l’inverse, le besoin de coder des choses triviales ou très connue devrait se réduire avec le temps et les techniques employées se déduire par référence à ce qui est utilisé dans l’écosystème.
[^] # Re: Typos, erreurs et preuves
Posté par thoasm . En réponse à la dépêche Sortie du Frido pour les Matheux. Évalué à 5.
Il y a plusieurs manières de gérer "l’habitude", soit tu utilises un théorème classique et dans ce cas une fois démontré il est dans une bibliothèque prêt à être utilisé, en principe ...
Soit il y a des "tactiques" connues qui sont codées dans l’assistant de preuve qui permettent de déduire une partie de la démonstration lui même, par exemple https://leanprover-community.github.io/mathlib_docs/tactic/linarith/frontend.html pour démontrer des choses sur des inégalités sans trop se fatiguer en principe ...
Ultimement et avec une bonne connaissance de l’écosystème, le côté "nouveau" ou "inhabituel" pourrait se déduire potentiellement du non emploi de ces techniques ou théorèmes pour démontrer des choses nouvelles. À l’inverse, le besoin de coder des choses triviales ou très connue devrait se réduire avec le temps et les techniques employées se déduire par référence à ce qui est utilisé dans l’écosystème.