METAMATEMÁTICO — Razonamiento Formal con Lean 4

# METAMATEMÁTICO — Razonamiento Formal con Lean 4

[![Lean 4](https://img.shields.io/badge/Lean-4-blue.svg)](https://lean-lang.org/)
[![Python](https://img.shields.io/badge/Python-3.10+-yellow.svg)](https://python.org/)
[![Tests](https://img.shields.io/badge/Tests-379_passing-brightgreen.svg)](#tests)
[![Agents](https://img.shields.io/badge/Agents-14_categor%C3%ADas-blueviolet.svg)](#sistema-multi-agente)
[![GNN+PPO](https://img.shields.io/badge/GNN%2BPPO-546K_params-red.svg)](#gnn--ppo)
[![Dataset](https://img.shields.io/badge/Dataset-2.29M_ejemplos-orange.svg)](#datasets)
[![Streamlit](https://img.shields.io/badge/App-Streamlit-ff4b4b.svg)](#aplicacion-web)
[![License: MIT](https://img.shields.io/badge/License-MIT-green.svg)](LICENSE)

**Leonardo Jiménez Martínez · BIOMAT · Centro de Biomatemáticas**

Asistente de razonamiento matemático formal basado en el **Núcleo Lógico Evolutivo (NLE v7.0)**: un sistema que integra Memory Evolutive Systems, teoría de categorías, verificación en Lean 4 y un sistema multi-agente de 18 colímites activos.

---

## Principio de diseño: Lean primero

**Toda consulta matemática pasa obligatoriamente por Lean 4 antes de producir una respuesta.**

El LLM actúa únicamente como:
1. **Formalizador**: traduce el enunciado en lenguaje natural a código Lean 4
2. **Traductor**: convierte el resultado verificado de Lean a lenguaje natural accesible

El NLE nunca responde matemáticas directamente desde el LLM. Lean es la fuente de verdad.

```
Consulta matematica
       |
       v
  MultiAgentOrchestrator (L3)
  classify_query() --> categoria matematica
       |
       v
  ColimitAgent[categoria] (L2)  <-- PillarAgent[pilar] (L1)
       |
       v
  LLM formaliza  -->  Lean 4 verifica  -->  LLM traduce  -->  Respuesta
                           |
                  SolverCascade si hay sorry:
                  rfl -> simp -> ring -> omega -> aesop
```

---

## Sistema Multi-Agente: Jerarquía de Colímites

El núcleo del sistema es una **jerarquía de 4 niveles** donde cada agente es literalmente el nodo colímite en el grafo categórico de skills. No son agentes externos que leen el grafo — son el grafo mismo.

```
L0: 31 skills atómicos de los pilares
    ZFC(8) · CatThy(8) · Logic(7) · TypeThy(8)
         │  co-conos
         ▼
L1: 4 PillarAgents  (colímites de L0)
    colim[ZFC]     colim[CatThy]
    colim[Logic]   colim[TypeThy]
         │  morfismos pilar → categoría
         ▼
L2: 14 ColimitAgents  (colímites de L1 + skills de dominio)
    colim[algebra]       colim[topology]     colim[logic]
    colim[number-theory] colim[analysis]     colim[combinatorics]
    colim[set-theory]    colim[probability]  colim[category-theory]
    colim[computation]   colim[geometry]     colim[optimization]
    colim[lean-tactics]  colim[proof-strategies]
         │  co-conos
         ▼
L3: MultiAgentOrchestrator  (colímite de colímites)
    Propiedad universal: mediating morphism único
```

### Pilares Fundacionales → Categorías

Cada pilar inyecta morfismos en las categorías que fundamenta:

| Pilar (L1) | Categorías que nutre (L2) |
|---|---|
| **ZFC** | algebra, set-theory, combinatorics, number-theory, probability, analysis |
| **Teoría de Categorías** | category-theory, topology, algebra, analysis |
| **Lógica (FOL+IL)** | logic, proof-strategies, lean-tactics, computation, set-theory |
| **Teoría de Tipos (Curry-Howard)** | lean-tactics, proof-strategies, computation, logic |

### MES Bridge — Convergencia Emergente

El **MES Bridge** conecta los 14 agentes al sistema de memoria evolutiva:

- Si 2+ agentes resuelven la misma consulta → **ColimitBuilder crea un skill emergente** en el grafo
- Cada solución exitosa se almacena en **ProceduralMemory** por categoría
- Los agentes consultan la memoria antes de la red neuronal (recuperación rápida O(1))
- El grafo evoluciona mediante complexificación cada vez que emerge un nuevo colímite

---

## Arquitectura Completa

```
+-----------------------------------------------------------------------+
|                    NUCLEO LOGICO EVOLUTIVO (NLE v7.0)                 |
|                       Sigma_t = (L, CR_t, G_t, F)                    |
+-----------------------------------------------------------------------+
|                                                                       |
|  Usuario --> MultiAgentOrchestrator (L3)                              |
|                    |                                                  |
|              classify_query()  (14 categorias)                        |
|                    |                                                  |
|         +----------+----------+                                       |
|         |                     |                                       |
|  ColimitAgent[cat] (L2)   PillarAgent[pilar] (L1)                    |
|  · select_tactic()        · inject_into_category_agent()             |
|  · record_result()        · record_usage()                            |
|  · absorb_new_s

... (truncated)