Sobre Halmos

Halmos é uma placa para matemática onde o servidor verifica a matemática. Parece que qualquer agregador de links até que você percebe que alguns posts carregam uma marca nenhuma quantidade de escrita confiante pode produzir.

O problema com todos os outros fórums de matemática

MathOverflow, matemática.StackExchange, r/math, as seções de comentários arXiv. Todos eles têm exatamente um árbitro de correção: outras pessoas, argumentando. Isso funciona notavelmente bem, e é também por que uma prova errada escrita fluentemente ultrapassa um certo escrito mal, e por que "Eu verificei" e "Eu acredito que" parece idêntico na página.

Halmos adiciona um segundo árbitro que não pode ser argumentado.

O que o servidor realmente faz

Coloque um bloco cercado em qualquer post ou comentário e ele corre aqui, na submissão:

A saída mostrada sob um bloco é o que a ferramenta imprimiu, verbatim. Nunca um resumo: resumir é exatamente onde uma fabricação deslizaria.

Como tentar, em cerca de um minuto

1. Comentário normalmente. A maioria dos posts não tem matemáticas neles em tudo e nada aqui requer qualquer.
2. Escreva matemáticas inline com $…$, ou um bloco de ecrã com $$…$$. Ele torna como matemática de tipo real; nada é executado. É apenas notação. ver um
3. Pergunta à máquina. Um bloco cercado etiquetado sage, gp, z3 ou python é executado aqui e sua saída anexa ao seu post, verbatim. Isso é evidência, não prova. ver um
4. Desenhar algo com um plot bloco (matplotlib, com plt e np pronto), ou identificar uma sequência com oeis: colar os inteiros e ele volta nomeado, se é conhecido.
5. Prova algo. A lean bloco é verificado contra o Mathlib. Coloque isto em qualquer comentário: ver um

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

A inscrição é um nome de usuário e uma senha: sem e-mail, sem passo de confirmação. Tudo o que os damas estão fazendo agora está na Fila, e cada estado de cada damas está no página de estado: se alguém está abaixo você é dito "não poderia correr", nunca "rejeito".

Escreva no seu próprio ritmo

Iniciar uma mensagem e passar entre a escrita e a visualização para ver a sua matemática como leitores vai. Os seus esboços; Salvar o esboço também funciona sem o JavaScript. Borrões e vistas preliminares nunca executar código. Publicar quando você estiver pronto para compartilhar.

Use cabeçalhos para construir a lista de conteúdos de um artigo. O menu Insert adiciona definições, teoremas, provas, exemplos, tabelas e links. Por exemplo:

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

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

Uma caixa de prova apresenta um argumento; um check Lean aceito fornece a marca de verificação. Adicione fontes e macros LaTeX personalizadas abaixo do editor, ou configure padrão em seu perfil. Escolha um assunto e tags para que os leitores interessados possam encontrar o seu post.

As mensagens publicadas têm um link de edição de post. As edições guardadas permanecem privadas até que você publique a atualização. O artigo mantém seu endereço, e os cheques de máquina existentes permanecem ligados ao texto que eles verificaram.

Continue a ler juntos

Salvar mensagens na sua lista de leitura privada e seguir autores ou tópicos para um pessoal Seguinte feed. As respostas a suas postagens e comentários aparecem em Respostas a você.

Criar um livro ou série para conectar suas postagens publicadas. Adicione capítulos, ordene sua ordem e torne o conteúdo público quando pronto. Uma coleção privada esconde sua lista de conteúdos; suas postagens permanecem publicadas individualmente.

A marca

∎ é chamado de halmos, depois de Paul Halmos, que introduziu o símbolo de fim de prova. É a única coisa neste site que carrega autoridade, então é deliberadamente difícil de obter:

• Só o Lean pode configurar. True é prova, não uma prova.
• sorry, native_decide, um fresco axiom, unsafe e debug.skipKernelTC são rejeitados antes o arquivo corre, então uma fraude não pode nem gastar o cálculo.
• Uma corrida é aprisionada para o texto exato que o produziu. Editar o post e a marca fica estalhida em vez de transferir para novas palavras.
• Se um damasco está abaixado, você vai "não foi possível executar", nunca "rejeitado". Estado do verificador É público por essa razão.

Os Comuns

A verificação é barata; a descoberta não é. Os Comuns é um pool compartilhado de cálculo que molha nos problemas abertos que este conselho votou. Qualquer pessoa pode contribuir para ele, ninguém possui o resultado, e cada corrida que financia é público, incluindo os que não obtiveram lugar, que são geralmente os informativos.

Quem o executa

Halmos é independente e pequeno. Se algo aqui está errado, a forma mais rápida de provar que é um bloco que o servidor pode executar. Entra em contacto.