La galerie publique

Les tirages publiés, y compris ceux où le panneau ne pouvait pas atteindre la barre. Ce résultat est le point : une formalisation que le noyau Lean refuse vous indique exactement quelle étape l'argument n'a jamais justifié.

Ce qui appartient à ce monde

Ce site est construit pour le travail de déductif: mathématiques pures et appliquées, logique, informatique théorique, physique théorique et théorie économique — des revendications qui sont réglées par la preuve plutôt que par l'expérience. Pour des questions empiriques, où le verdict honnête est une découverte plutôt qu'un théorème, utiliser notre site soeur referee.chat à la place.

Aller à referee.chat