En Lean 4 existen dos enfoques principales para construir demostraciones: el enfoque hacia atrás (backward) y hacia adelante (forward). Ambos son formas de construir el mismo término de prueba, pero difieren en la dirección en que razona el demostrador. En ocasiones, es útil usar un enfoque híbrido que combine los dos enfoques. BACKWARD PROOFS (PRUEBAS... Seguir leyendo →
Introducción a Lean 4 como lenguaje de tipos para las matemáticas
Lean 4 es un lenguaje de programación funcional y un asistente de pruebas interactivo basado en la teoría de tipos dependientes. Su fundamento lógico es el cálculo de construcciones con una jerarquía de universos e tipos inductivos . La idea central es que en matemáticas, cada objeto (un número, una función, una demostración) tiene un... Seguir leyendo →
IA, las matemáticas y Navier-Stokes
En los últimos días, después del anuncio de OpenAI de la resolución de varios de los casos del problema de Navier-Stokes (NS), hemos visto discusiones sobre la capacidad de la IA en las matemáticas y el futuro de las matemáticas. Es necesario recalcar, como hemos ido defendiendo en este sitio , las capacidades de los... Seguir leyendo →
