Baccare
Demuéstralo con Lean
Lean es un programa que revisa demostraciones matemáticas. Las universidades y los laboratorios de investigación lo usan para asegurarse de que los argumentos largos y difíciles no tengan huecos. Nosotros usamos un pedacito para enseñar algo para lo que cualquier niño de 10 u 11 años ya está listo: la diferencia entre "revisé algunos ejemplos" y "demostré que tiene que ser cierto".
Por qué presentar un revisor de demostraciones a esta edad
Los estándares de matemáticas de Texas les piden a los alumnos de 5.º y 6.º grado "justificar la solución", "analizar relaciones matemáticas" y "mostrar, explicar y justificar ideas y argumentos matemáticos con lenguaje matemático preciso". Esos son los estándares de proceso que atraviesan todos los grados, y son los más difíciles de practicar en una hoja de trabajo. Un revisor de demostraciones da retroalimentación inmediata e imparcial justo sobre esa habilidad: ¿el paso que escogiste de verdad estaba justificado? Además, Lean es la herramienta que los matemáticos del mundo ya usan para verificar investigaciones, así que un niño que la conoce a los 10 años la vuelve a encontrar en la universidad con ventaja.
Mantenemos el alcance chiquito a propósito. A este nivel, una demostración tiene tres o cuatro jugadas, todos los números son enteros y las demostraciones son sobre cosas que el niño ya cree (2 + 3 = 5, sumar cero no cambia nada, n + 1 es mayor que n). Lo nuevo no son las matemáticas. Lo nuevo es que "obviamente es cierto" hay que ganárselo.
Qué hay en el camino
by. Tu primera táctica, rfl: "los dos lados son lo mismo". Por qué Lean dice "goals accomplished" (metas cumplidas) y por qué rechaza 2 + 2 = 5.Jugar la actividad →theorem. Hipótesis. rw [h]: reescribe la meta usando algo que ya sabes. decide: deja que Lean resuelva una pregunta de sí o no. Qué quiere decir (n : Nat) y por qué una sola demostración puede cubrir todos los números.Jugar la actividad →intro, exact y omega. La idea del dominó detrás de la inducción: demuéstralo para 0, demuestra que cada número se lo pasa al siguiente, y una infinidad de casos caen de una vez. Por qué 0 + n = n es más difícil que n + 0 = n.Jugar la actividad →Cómo hacerlo en la mesa de la cocina
- Empiecen con un juego de escépticos, sin pantalla. Di "3 + 4 = 7". Pídele a tu hijo que te convenza sin calculadora. Luego ponte difícil: "¿Cómo sabes?". A cada respuesta que te dé, vuelve a preguntar. Esa sensación de quedarse sin "porque" es justo lo que arregla una demostración.
- Jueguen "Conoce Lean" juntos la primera vez. Lee en voz alta cada línea de Lean. Los dos puntos quieren decir "esto es lo que afirmo". El
:=quiere decir "y aquí está la demostración". La palabra que va después debyes la jugada. - Deja que digan el nombre de la jugada antes de tocar. "Los dos lados son iguales después de calcular" es
rfl. "Cambiar por algo que ya sé" esrw. "Nomás compruébalo" esdecide. Tres jugadas, tres oraciones. - Celebren una demostración rechazada. Cuando Lean rechaza 2 + 2 = 5, esa es toda la lección: el revisor no está del lado de nadie. Está del lado de lo que es cierto.
- Que le pregunten a Bacc si se atoran. Bacc conoce este camino y va a dar una pista sobre qué jugada va, nunca la respuesta.
Vocabulario, a la medida de los niños
- Meta: lo que intentas demostrar. Va entre los dos puntos y
:=. - Táctica: una jugada que cambia o termina una meta.
rfl,rw,decide,intro,exact,omega. - Hipótesis: un dato que puedes usar, con un nombre como
h. - Teorema: un dato demostrado con nombre, guardado para que otras demostraciones lo usen después.
- Nat: los números naturales 0, 1, 2, 3, … para siempre.
(n : Nat)quiere decir "n es cualquiera de ellos". - Inducción: el método del dominó. Demuéstralo para 0; demuestra que cada número se lo pasa al siguiente.
Opcional: prueben Lean de verdad, juntos
Lean tiene un área de prueba gratis en el navegador en live.lean-lang.org (en inglés). No necesita cuenta. Pega esto y mira el panel de la derecha:
example : 2 + 3 = 5 := by rfl example : 2 + 3 = 6 := by rfl -- Lean will complain here. Ask your child why. theorem add_zero_right (n : Nat) : n + 0 = n := by rfl
Este es un sitio externo que maneja la comunidad de Lean, no Baccare. Es adecuado para niños si están con un papá o una mamá al lado, pero no lo controlamos, y es una herramienta de programación completa con mucho más de lo que cubre este camino. El Natural Number Game (en inglés), también gratis y en el navegador, es el siguiente paso natural para un niño de 6.º grado que quiere más; convierte la inducción en un acertijo de nivel por nivel.
A dónde va esto
El camino se detiene en la inducción a propósito. El álgebra de secundaria es donde las variables, las ecuaciones y "para todo x" se vuelven trabajo de todos los días, y un alumno que ya conoció un revisor de demostraciones llega sabiendo que una ecuación es una afirmación, no una orden. Vamos a agregar niveles conforme se mapeen por completo los estándares de 6.º grado y conforme las familias nos digan qué funcionó.