Acerca de Halmos

Halmos es un tablero para las matemáticas donde el servidor comprueba las matemáticas. Parece cualquier agregador de enlaces hasta que note que algunos mensajes llevan una marca no cantidad de escritura segura puede producir.

El problema con cualquier otro foro de matemáticas

MathOverflow, matemáticas.StackExchange, r/math, las secciones de comentarios arXiv. Todos ellos tienen exactamente un árbitro de la corrección: otras personas, argumentando. Eso funciona notablemente bien, y es también por qué una prueba incorrecta escrita con fluidez supera a una correcta escrita mal, y por qué "lo comprobé" y "yo creo" se ven idénticos en la página.

Halmos añade un segundo árbitro que no puede ser discutido.

Lo que el servidor realmente hace

Ponga un bloque cercado en cualquier post o comentario y se ejecuta aquí, a petición:

Bloque	¿Qué pasa?	¿Puede ganar? ∎?
`lean`	Comprueba el tipo con Mathlib. El núcleo acepta el término prueba o no.	Sí
`sage`	SageMath lo ejecuta; la salida real se fija al poste.	No
`gp`	PARI/GP lo ejecuta.	No
`z3`	Z3 busca un modelo: la manera más rápida de refutar Algo.	No
`python`	Sandboxed Python, salida adjunta.	No

La salida que se muestra bajo un bloque es lo que la herramienta imprime, literalmente. Nunca un resumen: resumir es exactamente donde una fabricación se deslizaría.

¿Cómo probarlo, en un minuto

Observaciones normales. La mayoría de los posts no tienen matemáticas en absoluto y nada aquí requiere.
Escribe matemáticas en línea con $…$ , o un bloque de visualización con $$…$$. Renderiza como matemáticas reales; nada se ejecuta. Es sólo notación. ver uno
Pregúntele a la máquina. Un bloque cercado etiquetado sage, gp, z3 o python se ejecuta aquí y su salida adjunta a su post, literalmente. ver uno
Dibuja algo con una plot block (matplotlib, con plt y np listo), o identificar una secuencia con oeis: pegar los números enteros y vuelve a llamarse, si se conoce.
Demuéstrame algo. A lean bloque se comprueba de tipo contra Mathlib. Pegue esto en cualquier comentario: ver uno

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

El registro es un nombre de usuario y una contraseña: sin correo electrónico, sin paso de confirmación. Todo lo que las damas están haciendo ahora mismo está en el cola, y cada estado vivo de cada verificador está en el página de estado: si uno está abajo se le dice "no podría correr", nunca "rechazado".

Escribe a tu propio ritmo

Iniciar un puesto y cambiar entre la escritura y la vista previa para ver sus matemáticas como lo harán los lectores. Sus borradores; Guardar borrador también funciona sin JavaScript. Los borradores y las vistas previas nunca se ejecutan código. Publicar cuando esté listo para compartir.

Utilice encabezados para construir la lista de contenidos de un artículo. El menú Insertar añade definiciones, teoremas, pruebas, ejemplos, tablas y enlaces. Por ejemplo:

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

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

Una caja de pruebas presenta un argumento; una verificación Lean aceptada suministra la marca de verificación. Añadir fuentes y macros LaTeX personalizadas debajo del editor, o establecer valores predeterminados en tu perfil. Elija un tema y etiquetas para que los lectores interesados puedan encontrar su post.

Las publicaciones publicadas tienen un enlace de edición de publicaciones. Las ediciones guardadas permanecen privadas hasta que publiques la actualización. El artículo mantiene su dirección, y las comprobaciones de máquinas existentes permanecen atadas al texto que comprobaron.

Sigue leyendo juntos

Guardar mensajes en su lista de lectura privada y seguir a los autores o temas para un personal A continuación feed. Las respuestas a sus mensajes y comentarios aparecen en Respuestas a usted.

Crear un libro o una serie para conectar sus publicaciones. Añada capítulos, organice su orden y haga públicos los contenidos cuando esté listo. Una colección privada oculta su lista de contenidos; sus publicaciones se publican individualmente.

La marca

∎ se llama a halmos, después de Paul Halmos, que introdujo el símbolo de final de prueba. Es la única cosa en este sitio que lleva la autoridad, por lo que es deliberadamente difícil de conseguir:

Sólo Lean puede configurarlo. Impresión de salvia True es una prueba, no una prueba.
sorry, native_decide, una fresca axiom, unsafe y debug.skipKernelTC se rechazan antes el archivo se ejecuta, por lo que un tramposo ni siquiera puede gastar la computación.
Una ejecución se fija al texto exacto que lo produjo. Editar el post y la marca se va rancio en lugar de transferir a nuevas palabras.
Si un chequero está abajo, usted consigue "no se pudo ejecutar", nunca "rechazada". Estado del verificador es público por esa razón.

Los Comunes

La verificación es barata; el descubrimiento no lo es. Los Comunes es un grupo compartido de computación que muele en los problemas abiertos que este consejo ha votado. Cualquiera puede contribuir a ella, nadie posee el resultado, y cada ejecución de los fondos es pública, incluyendo los que no llegaron a ninguna parte, que son generalmente los informativos.

¿Quién lo dirige?

Halmos es independiente y pequeño. Si algo aquí está mal, la manera más rápida de demostrar que es un bloque que el servidor puede ejecutar. Póngase en contacto.