Post

Thomas🪴
@lipsum.dev

Cette politique de Lean (ne pas chercher à être minimaliste dans les axiomes utilisés) me semble très discutable alors que les gens s'interrogent sur les axiomes utilisés dans la preuve du th. de Fermat générée par IA.

Thomas🪴@lipsum.dev

Bon, et bien ma PR a été rejetée : > As discussed, reducing axioms beyond the three standard axioms is not a goal of the Lean standard library, and neither is the proofs being useful pedagogically. So I'm closing this PR. Je ne regrette pas de l'avoir proposée, car ça m'a permis de mieux comprendre

0 reposts0 likes

Thomas🪴
@lipsum.dev

Dans ce cas, il s'agit peut-être plus de questions d'univers (de Grothendieck) qui ne se traduisent pas en axiomes au sens de Lean, mais de façon générale la question de savoir ce qui est utilisé pour prouver tel résultat me semble tout à fait légitime.