Non. Le compilateur est sous Apache 2.0 (il y a juste leur application Web pour éditer collaborativement, un genre d'Overleaf, qui ne l'est pas, mais c'est indépendant, on peut compiler localement ou éditer sur une autre plateforme).
Breaking mathematical news: recent events have formally disproved the claim that adults are adults, refuting a nearly 350 years old conjecture of Leibniz. This is the first fully automated contribution to mathematics by autonomous geopolitical agents.
In French mathematics, families are tied into tribes living on separated spaces.
L'IA est effectivement devenue un énorme sujet de tension récemment, mais pas juste entre différents assistants de preuve, surtout à l'intérieur de la communauté Lean ainsi que celle d'Agda.
Cela dit, c'est moins habituel d'avoir ce genre de division en « tribus » dans la recherche en maths (et ça m'agace aussi en l'occurrence).
Bien sûr, mais quel rapport avec théorie des ensembles vs théorie des catégories ? Les deux ont des versions constructives parfaitement raisonnables (IZF/CZF, ETCS constructive de Palmgren), et de toute façon, Lean et Rocq ne sont fondés sur aucune des deux mais sur la théorie des types, alors…
Ça vient d'où ?? Je ne comprends absolument pas le rapport avec le schmilblick.
(Plus généralement, un sous-espace d'un espace polonais est polonais ssi il est G_δ.)
That's impossible, since the strait of Hormuz is not Polish.
No. The project was started before I switched fields and I wasn't going to let my collaborator down.
I asked on MathOverflow whether a certain corollary of the Cayley-Hamilton theorem can be interpreted from the point of view of algebraic geometry. Help appreciated, this would be very useful for a research project.
mathoverflow.net/q/510112/
Le critère de Lean est aussi ad-hoc mais moins restrictif et beaucoup plus simple (si je ne dis pas de bêtises, c'est le même que pour le Prop de Rocq), et en particulier il autorise l'élimination vers Type pour l'accessibilité.
L'élimination de SProp vers SProp ne pose pas de problème. L'élimination de SProp vers Type est restreinte aux inductifs satisfaisant un critère très ad-hoc, qui exclut notamment l'accessibilité (dont l'élimination vers Type donnerait effectivement des termes qui ne normalisent pas).
I asked on MathOverflow a very nice elementary algebraic geometry question that was posted here by @wildverzweigt.bsky.social: mathoverflow.net/q/510023/17064
Ça c'est plutôt un problème dans l'interaction entre SProp et Type.
(qui déjà ne termine pas toujours) ne serait potentiellement pas complet au sens où il existerait des termes théoriquement bien typés pour lesquels l'algo ne trouve pas de dérivation de typage.
repose sur une conjecture (l'injectivité de Π, c'est-à-dire que ∀ x : A, P(x) ≡ ∀ x : B, Q(x) implique A ≡ B et P ≡ Q où ≡ est l'égalité définitionnelle) qui pour cette théorie des types là est considérée difficile. Si elle était fausse, le semi-algorithme de type-checking
S'agissant de Lean, il implémente une théorie des types beaucoup plus petite (pas d'options funky), et il traduit la récursion en éliminateurs, donc a priori la correspondance avec le papier est beaucoup plus directe. Le truc (que peu de gens réalisent), c'est que l'algorithme de type-checking …
Du coup, il y a énormément d'options et ce n'est pas franchement possible de garantir qu'elles interagissent toutes bien. Par ailleurs le pattern matching d'Agda est très puissant et utile, mais comme en Rocq, il n'est pas traduit en éliminateurs et ce serait un boulot énorme d'implémenter ça.
S'agissant de Agda, ça a toujours été un endroit où tester des choses un peu expérimentales ou exotiques. (Par exemple, c'est la seule implémentation utilisable de la théorie des types cubique. Il y a aussi les inductifs-inductifs, sized types et bien d'autres choses.)
Pareil pour Prop vs SProp. Ils implémentent les deux par souci de compatibilité, mais le fait de les combiner n'est pas quelque chose de vraiment étudié sur papier parce qu'ils servent un peu la même fonction.
Maintenant ils ne peuvent plus revenir à quelque chose de mieux compris sans casser de l'existant. Il y a aussi les types coinductifs positifs, dont je suppose qu'ils aimeraient se débarrasser en faveur des types coinductifs négatifs. Là aussi ça casserait des développements existants.
Dans le cas de Rocq, il y a énormément de bagage historique. Par exemple, la condition de garde contient des choses à la justification théorique très douteuse pour faire passer des programmes à l'aspect raisonnable.
Je suppose qu'en géométrie algébrique c'est l'équivalent en sophistication de réduire une équation diophantienne mod 2 et mod 3, mais je suis curieux de savoir s'il y a une raison « évidente » pour laquelle ça ne peut pas marcher.
et qu'en bornant les degrés ceci est un système d'équations polynomiales en les coefficients de P, Q, A, B, qu'on doit pouvoir résoudre (disons sur les réels) par théorie de l'élimination ? Il n'aurait pas moyen de dérouler l'algorithme sur des degrés petits et observer ce qui se passe ?
J'ai du mal à croire qu'il faille des outils aussi sophistiqués pour ça. Je n'y ai pas réfléchi du tout mais : on est d'accord que la question est de savoir pour quels k il existe P, Q, A, B dans k[X, Y] tels que A*(X + P*(X^2 + Y^2 - 1)) + B*(Y + Q*(X^2 + Y^2 - 1)) = 1, …
Je dois aussi reconnaître très franchement qu'en général la littérature scientifique en théorie des types est dans un état assez déplorable, même si heureusement ça commence à s'améliorer doucement.
(Enfin, je parle de gros projets, parce qu'il existe plein d'implémentations jouet, peu utilisables.)
Après, si ton but est d'en apprendre plus sur les aspects théoriques, il n'y a pas besoin d'une implémentation pour ça (même si je reconnais que ça m'a beaucoup servi « quand j'étais jeune »…).
