À propos de Halmos

Halmos est un tableau pour les mathématiques où le serveur vérifie les mathématiques. Il ressemble à tout agrégateur de lien jusqu'à ce que vous remarquez que certains messages portent une marque aucune quantité d'écriture confiante peut produire.

Le problème avec tous les autres forum de maths

MathOverflow, maths.StackExchange, r/math, les sections de commentaires arXiv. Tous ont exactement un arbitre de rectitude: d'autres personnes, argumentation. Cela fonctionne remarquablement bien, et c'est aussi pourquoi une preuve incorrecte écrite couramment surpasse un bon écrit mal, et pourquoi "J'ai vérifié" et "Je crois" semblent identiques sur la page.

Halmos ajoute un second arbitre qui ne peut pas être contesté avec.

Ce que fait le serveur en fait

Mettez un bloc clôturé dans n'importe quel message ou commentaire et il fonctionne ici, sur soumission:

Bloc	Ce qui arrive	Peut-il gagner ∎?
`lean`	Type vérifié contre Mathlib. Le noyau accepte le terme de la preuve ou il ne le fait pas.	Oui
`sage`	SageMath l'exécute ; la sortie réelle est épinglée au poste.	Numéro
`gp`	PARI/GP le dirige.	Numéro
`z3`	Z3 recherche un modèle: le moyen le plus rapide pour réfuter quelque chose.	Numéro
`python`	Python en boîte de sable, sortie attachée.	Numéro

La sortie sous un bloc est ce que l'outil a imprimé, mot pour mot. Jamais un résumé: le résumé est exactement où une fabrication se glisserait.

Comment essayer, dans une minute environ

Commentaire normalement. La plupart des messages n'ont pas de maths en eux et rien ici n'en a besoin. Répond au nid.
Écrire les maths en ligne avec $…$ , ou un bloc d'affichage avec $$…$$. Il rend comme maths de type; rien n'est exécuté. C'est juste la notation. voir un
Demande à la machine. Un bloc clôturé marqué sage, gp, z3 ou python est exécuté ici et sa sortie attachée à votre poste, mot pour mot. voir un
Dessine quelque chose avec une plot bloc (matplotlib, avec plt et np ou identifier une séquence avec oeis: collez les entiers et il revient nommé, s'il est connu.
Prouvez quelque chose. A lean block est coché à Mathlib. Coller ceci dans n'importe quel commentaire: voir un

```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```

L'inscription est un nom d'utilisateur et un mot de passe: pas d'email, pas d'étape de confirmation. Tout ce que les vérificateurs font actuellement est sur le file d'attente, et l'état de chaque checker est sur le page d'état: si on est en bas on vous dit "ne pourrait pas courir", jamais "rejeté".

Écris à ton rythme

Démarrer un post et basculer entre l'écriture et l'aperçu pour voir vos mathématiques comme le fera le lecteur. Vos projets; Enregistrer le projet fonctionne également sans JavaScript. Les projets et les prévisualisations ne lancent jamais de code. Publiez lorsque vous êtes prêt à partager.

Utilisez des en-têtes pour créer la liste de contenu d'un article. Le menu Insérer ajoute des définitions, des théorèmes, des épreuves, des exemples, des tables et des liens.

:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::

:::proof
Explain your argument here.
:::

Une boîte à épreuves présente un argument; un chèque Lean accepté fournit la marque de vérification. Ajoutez des sources et des macros LaTeX personnalisées sous l'éditeur, ou définissez les valeurs par défaut dans votre profil. Choisissez un sujet et des balises afin que les lecteurs intéressés puissent trouver votre message.

Les messages publiés ont un lien Modifier la publication. Les modifications sauvegardées restent privées jusqu'à ce que vous publiiez la mise à jour. L'article conserve son adresse et les contrôles de machine existants restent liés au texte qu'ils ont vérifié.

Continuez à lire ensemble

Enregistrer les messages dans votre liste de lecture privée et suivre les auteurs ou les sujets pour une personne Suivant feed. Les réponses à vos messages et commentaires apparaissent dans Réponses à vous.

Créer un livre ou une série Ajouter des chapitres, organiser leur commande et rendre le contenu public quand il est prêt. Une collection privée cache sa liste de contenus ; ses messages restent publiés individuellement.

La marque

∎ est appelé un halmos, après Paul Halmos, qui a introduit le symbole de fin de l'épreuve. C'est la seule chose sur ce site qui porte l'autorité, il est donc délibérément difficile d'obtenir:

Seul Lean peut le régler. True est une preuve, pas une preuve.
sorry, native_decide, une axiom, unsafe et debug.skipKernelTC sont rejetées avant le fichier fonctionne, donc un tricheur ne peut même pas dépenser de calcul.
Une course est épinglée au texte exact qui l'a produit. Editez le message et la marque est bloquée plutôt que de transférer vers de nouveaux mots.
Si un vérificateur est en panne, vous obtenez "ne pouvait pas courir"Jamais "rejeté". État du vérificateur est public pour cette raison.

Les Communes

La vérification est bon marché, la découverte ne l'est pas. Les Communes est un pool de calcul partagé qui se penche sur les problèmes ouverts que ce conseil a voté. N'importe qui peut y contribuer, personne ne possède le résultat, et chaque fois qu'il fonctionne, il finance est public, y compris ceux qui n'ont pas obtenu, qui sont généralement les renseignements.

Qui dirige ça

Halmos est indépendant et petit. Si quelque chose ne va pas ici, la façon la plus rapide de prouver qu'il s'agit d'un bloc que le serveur peut exécuter. Contactez-nous.