Entonces vi que tenía que conmutarle a pensamiento Pro. Lo hice y entonces operó más tiempo, y construyó un contrajemplo que sí tenía sentido y me recordó que mi conjetura en realidad tenía que ver con solamente las dicotomías fuertes (es decir, que son autocomplementarias y de grupo de automorfismos trivial), no con el resto.
Le pregunté si podía demostrarse eso, trabajó otro rato, y dijo que sí. Que habría que desgranar por separado dos conteos (el del polinomio de inventario evaluado en $-1$ y otro explícito de las dicotomías). Era un desastre ininteligible, así que le di mis artículos sobre el tema y ya entonces reescribió el lado del conteo explícito en términos de las herramientas de mi artículo "Antichains and Counterpoint Dichotomies".
Ahora sí le ordené que intentara demostrarlo, y según que lo logró. Y ahí está la cuestión escabrosa, porque primero definió una función de Möbius univariable para un copo, lo cual no tenía sentido para mí. Resultó que obviaba un argumento evaluando siempre en el subgrupo trivial. Luego, la agrupación crucial de coeficientes del lado del conteo explícito no era clara. ¿Y está demostrado algo cuando no es lo suficientemente transparente cómo se logra? Seguramente se puede formalizar en Lean, pero para efectos de entender por qué está bien, ganaría nada.
Por ello me puse a escribir la demostración para entenderla.
- Para reducir a una cuestión booleana la acción de grupos que tienen al menos una órbita impar, el robot lo hizo en términos de una función característica. Tal vez funciona, pero al discutirlo resulta más fácil ver que esos grupos inducen otros que dividen a las órbitas en partes que son intercambiadas por las cuasipolaridades, haciendo obvias las potencias de 2 requeridas. Por cierto que aquí entendí para qué caracterizó esos grupos.
- Entonces retrabajé la caracterización de los grupos y así la demostración de la misma se puede reusar en parte para lo de las órbitas.
- Luego ya pude tratar de descifrar su agrupación de coeficientes, y empieza a verse bien el hilo conductor porque vuelve a salir la "extracción" de la parte "nuclear" de los grupos. Así ya pude reescribir todo el argumento en términos de corchetes de Iverson, y que lo hacen absolutamente transparente. Pienso que esto habría sido difícil de pulir en Lean, considerando mi experiencia de lo tiquismiquis que es con intercambios de sumas.
Por conversaciones subsecuentes con el robot infiero que él mismo no habría llegado a mis demostraciones, porque cuando le pedía revisar el manuscrito trataba de revertir todo a las suyas. Le pregunté por qué, y me dijo que porque así maximizaba la posibilidad de que no lo tronara la verificación formal.
Pero, si podemos escribir una demostración clara y correcta para un ser humano, relativamente mecánica en tanto notación según las enseñanzas de Knuth, entonces ¿para qué molestarse con una formal? Es más: con un buen lenguaje de programación, yo digo que esta demostración también es naturalmente formalizable.
Para mí esto confirma que no podemos simplemente dejar que el robot haga o deshaga y supuestamente convenza sin una auditoría mínima. Como bien se dice: se requiere la responsabilidad de al menos leer lo obtenido y saber que tiene un mínimo de coherencia. Aunque sean millones de líneas de código verificador, hay que pedirle que explique e interrogar su explicación.
Hay que resistir y hacer resistir, pues.
