Una IA puede proponer una demostración, pero una propuesta no es todavía una prueba comprobada. Formalizar significa escribir exactamente la afirmación y construir un objeto que siga reglas lógicas precisas. Empezaremos con dos hipótesis y una conjunción antes de estudiar qué valida el comprobador.
Si necesitas repasar:
1. Primero fijamos qué afirma la frase y sobre qué objetos
Una afirmación incluye dominio, operaciones, hipótesis y cuantificadores. «Todo entero impar tiene cuadrado impar» habla de enteros y de cualquier entero que cumpla la hipótesis. Cambiar enteros por reales sin definir imparidad no es una traducción equivalente.
Separaremos dos tareas: expresar fielmente la pregunta y justificar la afirmación formal resultante. Una derivación correcta para otra pregunta no resuelve la original. Los símbolos deben tener definiciones conocidas dentro del contexto.
Traducir impar sin dejarlo como una intuición
Un entero n es impar si existe k∈ℤ con n=2k+1.
Dominio
n y el testigo k son enteros.
Hipótesis
Se proporciona o se obtiene ese k.
Conclusión buscada
Debe existir otro entero j con n²=2j+1.
La palabra impar se convierte en una condición verificable.
No se exige que el mismo testigo k sirva para n².
Una construcción que vale para cualquier testigo
Suponemos n=2k+1.
Expandir
n²=4k²+4k+1.Elegir
j=2k²+2k es entero.Comprobar
2j+1=4k²+4k+1=n².
El testigo j demuestra la conclusión para cualquier entero k.
Un cálculo solo con n=3 no daría por sí mismo esta generalidad.
2. Una proposición puede verse como el tipo de sus pruebas
En el enfoque de proposiciones como tipos, hP:P significa que hP es una prueba de P. Un contexto Γ enumera las hipótesis y sus tipos. Escribimos Γ⊢t:C para decir que el término t demuestra C usando ese contexto.
Una prueba de P→Q es una construcción que recibe una prueba de P y produce una de Q. Para P∧Q se requieren ambas pruebas. Esta explicación usa notación esquemática de reglas; no estamos mostrando una ejecución de un asistente.
Aplicar una implicación
Disponemos de hP:P y hPQ:P→Q.
Entrada
hPQ necesita una prueba de P.
Aplicar
Le damos hP y obtenemos hPQ(hP).
Tipo
El resultado tiene tipo Q.
Es la regla de eliminación de la implicación, o modus ponens.
No se intercambian entrada y salida de hPQ.
Construir una implicación
Queremos P→P.
Suponer
Tomamos una prueba arbitraria h:P.
Devolver
Usamos esa misma prueba h.
Cerrar
La regla h↦h transforma cualquier prueba de P en una de P.
La identidad demuestra P→P sin suponer P como hecho externo.
La hipótesis h queda ligada dentro de la función, no libre en el resultado.
3. Una conjunción se construye con dos componentes y se usa proyectando
Con hP:P y hQ:Q formamos el par ⟨hP,hQ⟩ de tipo P∧Q. Una proyección izquierda recupera hP y una derecha recupera hQ. No se concluye que P y Q sean ciertas sin hipótesis: la prueba usa exactamente las dadas.
Podemos encadenar esas operaciones. Para demostrar (P∧Q)→(Q∧P), recibimos un par, extraemos sus componentes y las reconstruimos en el orden contrario. La estructura del término explica cada paso lógico.
Construir y recuperar
Contexto: hP:P, hQ:Q.
Construcción
t=⟨hP,hQ⟩:P∧Q.Izquierda
t.izq:P recupera hP.
Derecha
t.der:Q recupera hQ.
La prueba de la conjunción conserva las dos evidencias.
Una sola prueba de P no basta para obtener una Q arbitraria.
Intercambiar una conjunción
Objetivo (P∧Q)→(Q∧P).
Recibir
h:P∧Q.
Extraer
h.der prueba Q y h.izq prueba P.
Construir
h↦⟨h.der,h.izq⟩ tiene el tipo pedido.
La conclusión se deriva de reglas pequeñas y visibles.
No se ha añadido como axioma que la conjunción conmuta.
4. La IA y las tácticas proponen cómo construir la prueba
Una táctica aplica lemas, transforma objetivos o busca pasos. Una IA puede proponer tácticas o términos completos. La propuesta debe elaborarse y producir un término aceptado para el objetivo exacto. Su aspecto convincente no garantiza eso.
Un error puede indicar argumento equivocado, hipótesis ausente o afirmación falsa. Revisar el mensaje ayuda a corregir la construcción. La búsqueda puede ser muy compleja aunque las reglas del comprobador sean mucho más pequeñas.
Un paso algebraico propuesto que está mal
La propuesta afirma (x+y)²=x²+y² para todos los reales.
Probar un caso
x=y=1: izquierda 4, derecha 2.Detectar
Falta el término cruzado 2xy.
Corregir
La identidad correcta es x²+2xy+y², demostrable por distributividad.
Una propuesta plausible necesita comprobación.
La identidad falsa no se vuelve verdadera por escribirla con sintaxis formal.
Una hipótesis con otro tipo no encaja
Tenemos solo hQ:Q y el objetivo es P, sin otra relación entre ambas.
Propuesta
Usar hQ directamente.
Tipos
hQ tiene tipo Q, no P.
Lógica
El caso P falso y Q verdadero muestra que Q no implica una P arbitraria.
Hace falta una relación o evidencia adicional.
No se inventa una hipótesis para que la propuesta aparente funcionar.
5. El núcleo acepta una derivación relativa a definiciones y fundamentos
En asistentes como Lean, la elaboración resuelve notación y detalles; el núcleo comprueba el término con las definiciones, teoremas y axiomas del entorno. Esa separación permite que herramientas grandes propongan pasos y un mecanismo más pequeño valide la derivación.
La base de confianza no desaparece: importan lógica, implementación y contexto. Algunas vías de evaluación nativa añaden confianza en compilación u otros componentes. La afirmación precisa es qué enunciado se aceptó, con qué dependencias y mediante qué mecanismo.
El mismo texto puede referirse a definiciones distintas
Un archivo define Positivo(x) como x≥0, pero el lector interpreta x>0.
Cero
La definición del archivo acepta Positivo(0).
Intención
La desigualdad estricta del lector no lo acepta.
Revisión
Una prueba válida de la primera afirmación no demuestra la segunda.
Comprobar significado y comprobar derivación son tareas separadas.
Hay que leer definiciones y convenciones, además del nombre.
Dos modos de comprobar una cuenta
Una vía reduce un término según reglas del núcleo; otra usa una evaluación compilada admitida mediante dependencias adicionales.
Objetivo
Pueden buscar la misma igualdad aritmética.
Evidencia
Hay que saber qué mecanismo produjo la aceptación.
Auditoría
Se registra esa diferencia de confianza junto con las dependencias.
Más rapidez no hace idéntica la base de confianza.
No afirmamos que una ejecución concreta se haya realizado aquí.
6. Omitir la prueba o asumir la conclusión cambia lo demostrado
Un marcador de prueba omitida puede introducir una dependencia que representa lo que falta. En Lean se puede inspeccionar la lista de axiomas de un teorema y de sus dependencias con #print axioms; sorryAx indica una omisión. Una dependencia omitida también importa aunque el teorema actual parezca completo.
Los axiomas no son automáticamente errores: se trabaja respecto de fundamentos declarados. Lo que se revisa es que sean los acordados y que no se haya añadido inadvertidamente la conclusión o una contradicción.
Asumir C no prueba C desde el contexto original
El objetivo era demostrar Γ⊢C.
Cambiar
Se añade un nuevo axioma a:C.
Resultado
Ahora se puede usar a para obtener Γ,a:C⊢C.
Comparar
El contexto nuevo es más fuerte; falta la derivación desde Γ solo.
La conclusión se ha supuesto en lugar de demostrarla.
La aceptación relativa a ese contexto no demuestra que se conserve el problema original.
Una omisión puede estar en un lema usado
El teorema T usa un lema L cuya prueba quedó omitida.
Apariencia
Los pasos de T pueden estar completos.
Cadena
Su prueba depende de L y de la evidencia que a L le falte.
Revisar
Se inspeccionan las dependencias transitivas, no solo la última línea.
Una auditoría sigue toda la cadena de evidencia.
No se etiqueta como prueba completa mientras esa omisión siga siendo necesaria.
7. Los cuantificadores y las hipótesis deben coincidir con la pregunta
Para probar ∀x de un dominio se toma un x arbitrario y se razona sin restricciones no declaradas sobre él. Instanciar una prueba universal en x=2 es válido; convertir una comprobación solo en x=2 en una prueba universal no lo es.
Cambiar dominio, añadir una hipótesis o alterar la conclusión puede producir un teorema válido diferente. Una hipótesis imposible hace válida una implicación de manera vacía; eso exige revisar si la formalización sigue representando la intención.
Una instancia frente a todos los reales
Se pide ∀x∈ℝ, x²≥0.
Instancia
Comprobar 2²≥0 da una afirmación verdadera particular.Falta
No se ha construido una prueba para un real arbitrario.
General
El argumento de cuadrados no negativos debe justificarlo para cualquier real, incluido cero y los negativos.
La instancia no reemplaza el cuantificador universal.
Para obtener la instancia sí se podría usar después una prueba universal válida.
Una hipótesis imposible puede esconder el cambio
Se demuestra: si un real cumple x²<0, entonces 0=1.
Hipótesis
Ningún real cumple x²<0.Implicación
No hay un caso que satisfaga el antecedente y refute el consecuente.
Alcance
Esto no demuestra 0=1 sin esa hipótesis.
La validez de una implicación vacía no valida una traducción arbitraria.
Se revisa qué hipótesis tenía realmente el problema.
8. Un registro permite repetir la comprobación de la misma afirmación
Conservamos enunciado, definiciones e hipótesis, término o archivo de prueba, versiones del asistente y bibliotecas y dependencias usadas. Se comprueba sin omisiones y se inspeccionan axiomas. Si corresponde, una revisión independiente vuelve a comprobar el objeto guardado.
Proponer, comprobar y explicar son tareas diferentes. Un resultado externo puede incorporarse mediante un certificado cuando exista un verificador adecuado; copiar su número final no basta para convertirlo en un teorema.
Un certificado pequeño de reglas proposicionales
Guardamos la construcción h↦⟨h.der,h.izq⟩.
Enunciado
Se fija (P∧Q)→(Q∧P), con P,Q proposiciones arbitrarias.Comprobar
Cada proyección tiene el tipo requerido y el par tiene tipo Q∧P.
Conservar
La construcción se guarda con la definición de esas reglas para poder revisarla.
La evidencia es el objeto y su tipado, no solo una etiqueta de éxito.
El pequeño verificador proposicional de esta muestra no es Lean ni verifica su lógica completa.
Conectar una búsqueda con una comprobación
Un programa sugiere 221=13·17.
Buscar
El procedimiento que encontró factores puede ser complejo.
Verificar
Una multiplicación exacta confirma 13·17=221 y ambos factores son no triviales.
Incorporar
Una prueba formal necesitaría expresar esa identidad y comprobarla mediante las reglas del sistema elegido.
Un certificado separa búsqueda de verificación.
La multiplicación aquí no se presenta como un teorema ejecutado en Lean.
9. Una prueba de la afirmación no resuelve todas las preguntas sobre ella
Una derivación formal bien comprobada aporta evidencia fuerte sobre la afirmación especificada. No demuestra automáticamente que un modelo represente la realidad, que los datos sean correctos ni que la explicación sea comprensible.
La IA puede ayudar a buscar, traducir o explicar, manteniendo visibles pregunta, contexto y objeto comprobado. El objetivo pedagógico sigue siendo entender por qué cada paso es válido y qué conclusión permite.
Modelo correcto por dentro y datos discutibles
Se demuestra que un coste cuadrático con coeficiente positivo tiene un mínimo único.
Teorema
La derivación puede ser exacta para esa función.
Modelo
Todavía hay que justificar que esa función describa la situación estudiada.
Datos
Un coeficiente estimado con error no queda validado por la prueba simbólica.
Corrección lógica y adecuación de un modelo son preguntas distintas.
La prueba no promete exactitud de medidas que no forman parte de sus hipótesis.
Una prueba completa puede necesitar una explicación adicional
Se entrega un término aceptable pero sin nombres ni motivación legibles.
Comprobación
Sus reglas pueden validarse.
Comprensión
El lector todavía necesita identificar ideas, datos y pasos.
Enseñar
Se reconstruye la explicación conservando el mismo enunciado y las mismas condiciones.
Verificar y enseñar se complementan.
Simplificar una explicación no autoriza a cambiar el alcance de lo probado.
Ahora lo resolvemos de principio a fin.
EJEMPLO RESUELTO 1
Construir una conjunción
Dispones de hP:P y hQ:Q. ¿Qué falta para demostrar P∧Q?
Hipótesis
hP:P y hQ:Q están disponibles en el contexto.
Objetivo
P∧Q requiere una prueba de cada componente.
Primera
Usamos hP para P.
Segunda
Usamos hQ para Q.
Construir
El par ⟨hP,hQ⟩ tiene tipo P∧Q.
Comprobar
Sus proyecciones recuperan las hipótesis; no se han eliminado los supuestos.
El par demuestra P∧Q.
Proyectar su primera y segunda componentes recupera las hipótesis.
EJEMPLO RESUELTO 2
Detectar una formalización equivocada
El problema pide ∀x real, x²≥0, pero se formaliza solo 2²≥0. ¿Resuelve el problema?
Problema
Se pide ∀x real, x²≥0.Traducción propuesta
Solo afirma 2²≥0.Diferencia
El número 2 es una elección particular, no un real arbitrario.
Validez local
La cuenta 4≥0 sí es correcta.Insuficiencia
No prueba el enunciado universal pedido.
Corregir
Se conserva el dominio real y el cuantificador para todos al construir la prueba general.
No; falta la afirmación general.
La fidelidad del enunciado se revisa además de la validez del término.
Los símbolos que hemos usado
- Enunciado formal
- Proposición escrita con tipos, dominios, cuantificadores y definiciones precisos.
- Contexto
- Hipótesis y declaraciones disponibles para una demostración.
- Término de prueba
- Objeto cuya comprobación de tipo establece una proposición en el sistema.
- Núcleo
- Componente que comprueba el término según las reglas fundacionales.
- Táctica
- Procedimiento que construye términos o transforma objetivos de prueba.
- Axioma
- Afirmación asumida en el sistema o contexto, en lugar de derivada.
- Fidelidad
- Correspondencia entre el enunciado formal y la pregunta matemática original.
Ahora te toca a ti.
Tienes cinco ejercicios. Inténtalos; las pistas te ayudan si te atascas.
Practicar este tema →