METAMATEMÁTICO — Razonamiento Formal con Lean 4
Leonardo Jiménez Martínez · BIOMAT · Centro de Biomatemáticas
Repositorio completo: GitHub — Metamatemático
Instalación y uso rápido del modelo
ash pip install torch>=2.5.1 torch-geometric>=2.7.0 huggingface-hub>=0.31
`python from huggingface_hub import hf_hub_download import importlib.util
Descargar model.py desde este repositorio
model_py = hf_hub_download("metamatematico/Metamatematico", "model.py") spec = importlib.util.spec_from_file_location("model", model_py) mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod)
Instanciar con descarga automática de pesos
model = mod.MetamaticoPredictor.from_pretrained()
Predecir acción para una consulta matemática
result = model.predict("Prove that the square root of 2 is irrational") print(result["action"]) # ASSIST → ruta al pipeline Lean 4 print(result["confidence"]) # 1.0 print(result["probabilities"])
{"RESPONSE": 0.0, "REORGANIZE": 0.0, "ASSIST": 1.0}
`
Acciones que predice el modelo
| Acción | Descripción |
|---|---|
| ASSIST | Enviar al pipeline de verificación formal en Lean 4 (la mayoría de problemas matemáticos) |
| RESPONSE | Responder directamente sin verificación formal (saludos, preguntas generales) |
| REORGANIZE | Reestructurar el grafo interno de conocimiento |
Archivos en este repositorio
| Archivo | Descripción |
|---|---|
| model.py | Clase standalone para inferencia — sin dependencias del NLE completo |
| xample.py | 5 ejemplos listos para ejecutar |
| equirements.txt | Dependencias mínimas (3 líneas) |
| eural_agent.pt | Pesos del modelo (versión final post-PPO Lean, 2.2 MB) |
| est.pt | Mejor checkpoint supervisado (época 10, val_acc=1.0) |
| config.json | Hiperparámetros de arquitectura |
| raining_log.json | Log completo del entrenamiento |
| src/gnn.py | SkillGNN integrado con el grafo NLE |
| src/networks.py | ActorCriticNetwork integrado con el NLE |
| src/agent.py | NucleoAgent con PPO, memoria procedimental y epsilon-greedy |
Índice
- Qué es este sistema
- El cerebro formal: NLE + Lean 4
- Sistema Multi-Agente: Jerarquía de Joins
- Memory Evolutive Systems (MES)
- Red Neuronal GNN + PPO
- Co-Reguladores
- Cómo funciona: flujo completo de una consulta
- Tests
- Datasets
- Aplicación Web
- Entrenamiento
- Estructura del Repositorio
- Instalación
- Fundamento Teórico
1. Qué es este sistema
Metamatemático es un asistente de razonamiento matemático formal. A diferencia de un LLM convencional que genera texto plausible, este sistema verifica matemáticamente cada respuesta antes de producirla.
El núcleo se llama NLE v7.0 (Núcleo Lógico Evolutivo). Combina cuatro disciplinas en una arquitectura donde el LLM es solo la interfaz de lenguaje, mientras que el NLE y Lean 4 constituyen el cerebro formal:
| Componente | Rol |
|---|---|
| NLE (Núcleo Lógico Evolutivo) | El cerebro: clasifica la consulta, activa el agente especializado del área, ordena las tácticas Lean, aprende de cada interacción y coordina todo el sistema |
| Lean 4 | El juez formal: verifica que la afirmación matemática sea correcta. Su veredicto es inapelable |
| LLM (Claude, DeepSeek, Gemini…) | La boca: formaliza la consulta en Lean y traduce el resultado verificado a lenguaje natural. No razona por sí solo |
Principio fundamental: el LLM nunca produce matemáticas directamente. Toda respuesta matemática — sea una demostración, una definición, o una explicación conceptual — pasa por Lean antes de llegar al usuario.
2. El cerebro formal: NLE + Lean 4
Por qué Lean como fuente de verdad
Los modelos de lenguaje pueden generar demostraciones que suenan correctas pero contienen errores sutiles. Lean 4 es un lenguaje con tipos dependientes que actúa como verificador: si compila sin errores, la demostración o definición es matemáticamente correcta.
Este sistema garantiza que el LLM nunca pueda inventar matemáticas porque su rol está arquitecturalmente limitado a:
- Escribir código Lean (formalizar) — antes de que Lean lo verifique
- Traducir el resultado de Lean a palabras — después de que Lean lo verifique
Dos tipos de formalización
| Tipo de query | Qué genera Lean | Ejemplo |
|---|---|---|
| Prueba | heorem / lemma con táctica | "Demuestra que √2 es irracional" |
| Definición | #check / structure / class | "¿Qué es una CCC?" |
Para definiciones, el sistema genera código como:
lean import Mathlib.CategoryTheory.Closed.Cartesian #check CartesianClosed -- eval : B^A × A → B (no C^A — el exponencial es B^A) #check CategoryTheory.CartesianClosed.curry -- curry : Hom(C × A, B) ≅ Hom(C, B^A)
SolverCascade con táctica por área
Cuando la formalización contiene sorry, el ColimitAgent del área detectada aporta la táctica con mayor probabilidad de éxito, que se coloca primera en la cascada:
| Área | Táctica por defecto |
|---|---|
| algebra | |
| ing | |
| number-theory | |
| orm_num | |
| logic | auto |
| optimization | linarith |
| lean-tactics | simp |
| computation | decide |
| topology / analysis | continuity |
3. Sistema Multi-Agente: Jerarquía de Joins
Principio 3.1 — Separación proceso/objeto
El agente ENVUELVE el join — no ES el join.
El sistema tiene 19 join-envoltorios en 3 niveles:
L3: 1 Orchestrator ← join-envoltorio del sistema completo ↑ L2: 14 join-envoltorios ← uno por área matemática (algebra, topology, …) ↑ L1: 4 PillarAgents ← ZFC · CatThy · Logic · TypeThy ↑ L0: 76 skills atómicos ← los objetos del grafo (no agentes)
La jerarquía de 4 niveles
L0: 76 skills atómicos (fundamentos + dominios + estrategias) ┌──────────────────────────────────────────────────────┐ │ ZFC (8) │ CatThy (8) │ Logic (7) │ TypeThy (8) │ (10 L0) │ + 66 skills de dominio distribuidos en 14 categorías │ └──────────────────────────────────────────────────────┘ │ co-conos verificados por is_join() ▼ L1: 4 PillarAgents — join-envoltorios de sus skills L0 join[ZFC] join[CatThy] join[Logic] join[TypeThy] │ morfismos L1 → L2 ▼ L2: 14 join-envoltorios de área join[algebra] join[analysis] join[category-theory] join[combinatorics] join[computation] join[geometry] join[lean-tactics] join[logic] join[number-theory] join[optimization] join[probability] join[proof-strategies] join[set-theory] join[topology] │ co-conos hacia L3 ▼ L3: Orchestrator — join-envoltorio de los 14 joins de área
Qué pilares fundamentan cada área
| Pilar L1 | Áreas L2 que nutre | Por qué |
|---|---|---|
| ZFC | algebra, set-theory, combinatorics, number-theory, probability, analysis | Toda la matemática clásica se construye sobre conjuntos |
| Teoría de Categorías | category-theory, topology, algebra, analysis | Espacios topológicos, funtores y trans. naturales son objetos categóricos |
| Lógica (FOL+IL) | logic, proof-strategies, lean-tactics, computation, set-theory | Las reglas de deducción dependen de la lógica formal |
| Teoría de Tipos (Curry-Howard) | lean-tactics, proof-strategies, computation, logic | Lean 4 está basado en CIC — las pruebas son programas |
Cómo un join-envoltorio selecciona una táctica
select_tactic(query) sigue 5 pasos en cascada:
| Paso | Fuente | Descripción |
|---|---|---|
| 1 | Memoria procedimental | Hash exacto de la query: si este problema fue resuelto antes, devuelve la táctica exitosa |
| 2 | Morfismo mediador | Si otro agente resolvió una query similar con táctica compartida, está en _mediating_memory |
| 3 | Co-cono ponderado | Activa skills relevantes ponderados por peso de morfismo hacia el join |
| 4 | Señal de pilar (L1→L2) | Lee morfismos L1→L2, detecta keywords del pilar dominante |
| 5 | domain_default_tactic | Tabla estática por área: algebra→ |
| ing, number-theory→ | ||
| orm_num, etc. |
MES Bridge — extensión del grafo y skills emergentes
join-env[algebra] ──→┐ join-env[number-theory]→┤ MES Bridge join-env[...] ──→┘ │ record_success(query, tactic, reward) │ ┌────────┴────────┐ │ │ ProceduralMemory PatternManager por área detecta convergencia: (O(1) lookup) ¿2+ agentes resolvieron la misma query? │ ▼ ColimitBuilder is_join() verifica propiedad universal → nuevo nodo en G_t (extensión del grafo)
4. Memory Evolutive Systems (MES)
Los Memory Evolutive Systems (Ehresmann) modelan cómo el conocimiento crece manteniendo coherencia estructural.
Los tres conceptos clave
Patrón P: I → K Selección de skills relevantes para un tipo de problema. Funtor de una categoría índice I hacia el grafo K.
join[P] — cota superior mínima verificada El join del patrón en la categoría thin G es el skill emergente que los sintetiza. is_join() verifica explícitamente la propiedad universal: todo objeto que recibe morfismos de todos los componentes del patrón se factoriza de manera única a través de join[P].
Nota: el reclamo matemático es que join[P] es la cota superior mínima en la subcategoría thin finita G_n (~76-100 skills). No se reclama colímite en el sentido de CategoryTheory.Limits.IsColimit de Mathlib — esa conexión formal es trabajo futuro.
Extensión del grafo K' Cuando el sistema añade join[P] con sus co-conos, el grafo pasa de K a K'. El conocimiento crece sin destruir la estructura anterior.
Axiomas implementados y Teoremas verificados
| Axioma/Teorema | Descripción | Suite de tests |
|---|---|---|
| 8.1 Jerarquía | Skills en niveles L0 < L1 < L2 | est_patterns.py |
| 8.2 Multiplicidad | Un skill puede pertenecer a múltiples patrones | est_patterns.py |
| 8.3 Conectividad | Los patrones son conexos en el grafo | est_patterns.py |
| 8.4 Cobertura | Los pilares cubren todas las categorías | est_pillar_agents.py |
| 8.5 Emergencia | Si el patrón existe, el join existe y es único | est_colimit_agents.py |
| 8.6 Absorción | Nuevos skills se integran sin destruir joins previos | est_colimit_agents.py |
| 8.7 Mediación | Entre dos joins con solución común existe morfismo mediador único | est_colimit_agents.py |
Memoria procedimental
Sembrada inicialmente con 2,371 patrones de ProofNet y NuminaMath. Crece con cada interacción:
python { "query_text": "prove that n^2 + n is even", "tactic_used": "omega", "lean_goal": "⊢ ∀ n : ℕ, 2 ∣ n^2 + n", "reward": 1.0, "category": "number-theory" }
5. Red Neuronal GNN + PPO
Arquitectura
Entrada: query (texto) + grafo de skills (PyG) │ ▼ encode_query() encode_goal() bag-of-keywords hash determinístico → VOCAB_SIZE(35) → 32-dim │ │ └──────────┬───────────┘ │ SkillGNN (3 × GATConv + LayerNorm + Dropout): input_proj → NODE_FEAT(9) × 256 GATConv 1 → 256 × 256 × 4 heads (edge_dim=6) GATConv 2 → 256 × 256 × 4 heads GATConv 3 → 256 × 256 × 4 heads global_mean_pool → graph_embedding (256) │ ActorCriticNetwork: QueryEncoder → 35 × 128 × 256 GoalEncoder → 32 × 128 × 256 Fusion → 768 → 256 → LayerNorm Actor → 256 → 128 → 3 (logits) Critic → 256 → 128 → 1 (value) │ Acción: ASSIST (→ Lean 4) | RESPONSE (→ directo) | REORGANIZE (→ grafo)
Total: 546,820 parámetros — 2.2 MB
Resultados de entrenamiento
Fase 1 — Supervisado:
| Métrica | Resultado |
|---|---|
| Dataset | 52,237 train · 6,552 val · 12,874 test |
| Fuentes | MATH + GSM8K + NuminaMath + ProofNet |
| Épocas | 15 (converge en época 1) |
| train_acc / val_acc / test_acc | 100% / 100% / 100% |
Fase 2 — PPO con recompensas reales de Lean (5 épocas, RTX 3050):
| Época | Loss | Avg Reward |
|---|---|---|
| 1 | 0.0746 | 0.573 |
| 2 | 0.0253 | 0.570 |
| 3 | 0.0163 | 0.562 |
| 4 | 0.0191 | 0.587 |
| 5 | 0.0172 | 0.578 |
El reward ~0.57 refleja la distribución real: ~70% aritmética ( orm_num → 1.0) y ~30% álgebra abstracta (→ 0.5).
Aprendizaje vivo
Cada interacción actualiza el sistema:
Consulta → join-env selecciona táctica → Lean verifica → record_result(reward) → memoria procedimental actualizada → Transition → buffer PPO → cada 10 interacciones: agent.update() + save weights
6. Co-Reguladores
4 co-reguladores controlan el flujo antes de llegar a los join-envoltorios:
| Co-regulador | Umbral | Función |
|---|---|---|
| TACTICAL (CR_tac) | 80% del tráfico | Clasifica la consulta: ¿pipeline Lean-primero o respuesta directa? |
| ORGANIZATIONAL (CR_org) | Multi-paso | Organiza secuencia de tácticas en demostraciones largas |
| STRATEGIC (CR_str) | 20% del tráfico | Decide estrategia global: backward reasoning, casos, inducción |
| INTEGRATIVE (CR_int) | Resultados parciales | Integra sub-demostraciones en una prueba coherente |
7. Cómo funciona: flujo completo de una consulta
NLE + Lean = cerebro. LLM = boca.
┌──────────────────────────────────────────────────────────────────────┐ │ USUARIO: "¿Qué es una CCC?" / "Demuestra que √2 es irracional" │ └──────────────────────┬───────────────────────────────────────────────┘ │ ▼ ┌──────────────────────────────────────────────────────────────────────┐ │ PASO 1 — ¿Es matemática? │ │ 80+ palabras clave, símbolos Unicode (∀∃∈ℝ), LaTeX │ │ NO → respuesta directa LLM SÍ → Paso 2 │ └──────────────────────┬───────────────────────────────────────────────┘ ▼ ┌──────────────────────────────────────────────────────────────────────┐ │ PASO 2 — Co-Reguladores votan la estrategia │ │ CR_tac · CR_org · CR_str · CR_int → acción: ASSIST o RESPONSE │ └──────────────────────┬───────────────────────────────────────────────┘ ▼ ┌──────────────────────────────────────────────────────────────────────┐ │ PASO 3 — Clasificación de área y join-envoltorio especializado │ │ classify_query(text) → área (14 categorías, español + inglés) │ │ "¿Qué es una CCC?" → area: "category-theory" │ │ "Demuestra √2 irracional" → area: "number-theory" │ └──────────────────────┬───────────────────────────────────────────────┘ ▼ ┌──────────────────────────────────────────────────────────────────────┐ │ PASO 4 — ¿Prueba o Definición? │ │ "qué es", "define" → path DEFINITIONAL (#check / structure) │ │ "demuestra", "prueba" → path PRUEBA (theorem/lemma + sorry) │ └──────────────────────┬───────────────────────────────────────────────┘ ▼ ┌──────────────────────────────────────────────────────────────────────┐ │ PASO 5 — Lean 4 verifica el código │ │ ✅ ÉXITO → confianza 95% │ │ ⚠ SORRY → SolverCascade con domain_tactic primero │ │ ❌ ERROR → diagnóstico estructurado de tipo de error │ └──────────────────────┬───────────────────────────────────────────────┘ ▼ ┌──────────────────────────────────────────────────────────────────────┐ │ PASO 6 — LLM traduce lo que Lean verificó │ │ La explicación DEBE ser consistente con los tipos del código Lean │ └──────────────────────┬───────────────────────────────────────────────┘ ▼ ┌──────────────────────────────────────────────────────────────────────┐ │ RESPUESTA: [Explicación] + "Lean 4 ✓ · área: number-theory" │ └──────────────────────┬───────────────────────────────────────────────┘ ▼ ┌──────────────────────────────────────────────────────────────────────┐ │ PASO 7 — Aprendizaje: reward → PPO buffer → memory.json │ │ Pesos actualizados cada 10 interacciones │ └──────────────────────────────────────────────────────────────────────┘
8. Tests
ash git clone https://github.com/metamatematico/Metamatematico---Razonamiento-Formal-con-Lean.git cd Metamatematico---Razonamiento-Formal-con-Lean python -m pytest tests/ -o "addopts=" -v
382 tests en 18 suites, organizadas por subsistema:
| Suite | Tests | Qué verifica |
|---|---|---|
| est_colimits.py | 28 | Propiedad universal, co-conos, morfismo mediador |
| est_evolution.py | 22 | Extensión del grafo, snapshots, functores de transición |
| est_emergence.py | 18 | Links simples/complejos, detección de emergencia |
| est_multiplicity.py | 15 | Principio de multiplicidad |
| est_co_regulators.py | 20 | 4 CRs activos, E-equivalencia |
| est_gnn.py | 25 | SkillGNN forward pass, graph_to_pyg() |
| est_ppo.py | 18 | PPO update, GAE, clipping |
| est_lean.py | 30 | Cliente Lean 4, SolverCascade, sorry analyzer |
| est_memory.py | 22 | MES Memory, patrones procedimentales |
| est_live_learning.py | 10 | Chat → PPO → weights update ciclo completo |
| est_cli.py | 10 | python -m nucleo chat REPL |
| est_multi_agent.py | 35 | join-envoltorios, PillarAgent, MES Bridge, classify_query() |
| est_patterns.py | 26 | Axiomas 8.1–8.4, Teoremas 8.5–8.7, is_join() |
| est_math_domains.py | 32 | 76 skills en 14 categorías |
| est_domain_tactic_pipeline.py | 30 | classify_query ES+EN, domain_default_tactic, try_fill_sorry_smart |
| + 3 suites auxiliares | ~41 | Config, types, eval, graph base |
9. Datasets
El sistema integra 5.4M+ ejemplos matemáticos de datasets públicos:
| Dataset | Ejemplos | Categorías |
|---|---|---|
| OpenMathReasoning | 3,201,061 | algebra, number-theory, analysis, competition math |
| NuminaMath | 859,494 | algebra, combinatorics, number-theory, geometry |
| MetaMathQA | 395,000 | algebra, arithmetic |
| Autoformalization | 327,000 | lean-tactics (pares NL ↔ Lean) |
| OrcaMath | 200,000 | algebra, arithmetic |
| OpenR1Math | 93,000 | proof-strategies |
| LeanWorkbook + Proofs | 54,000 | lean-tactics (pruebas Lean reales) |
| BigBench Formal Fallacies | 14,200 | logic |
| HendrycksMath | 12,500 | algebra, calculus, statistics |
| OmniMath | 4,400 | IMO, APMO, Putnam |
| ProofNet | 371 | proof-strategies, lean-tactics |
| GSM8K + MATH + miniF2F | ~21,000 | aritmética, álgebra |
10. Aplicación Web
ash git clone https://github.com/metamatematico/Metamatematico---Razonamiento-Formal-con-Lean.git cd Metamatematico---Razonamiento-Formal-con-Lean pip install -r requirements.txt PYTHONIOENCODING=utf-8 streamlit run app.py
Abre en http://localhost:8501.
Proveedores LLM soportados
| Proveedor | Modelos | Costo |
|---|---|---|
| Anthropic | Claude Haiku 4.5, Claude Sonnet 4.6 | De pago |
| DeepSeek | deepseek-chat (V3), deepseek-reasoner (R1) | De pago (muy barato) |
| Google AI Studio | Gemini 2.0 Flash, Gemini 1.5 Pro | Gratis (con cuota) |
| Groq | Llama 3.3 70B, Mixtral 8x7B | Gratis |
| Demo | Contenido matemático local | Sin key |
Funcionalidades
| Funcionalidad | Descripción |
|---|---|
| Chat multi-turno | Conversación continua con memoria interna del NLE |
| Adjuntar archivos | .txt, .tex, .pdf — pipeline de verificación de 6 pasos |
| Visualizaciones | Grafo de skills, embeddings t-SNE/PCA, diagrama MES, árbol de agentes |
| Verificador Lean 4 | Editor con verificación en tiempo real |
| Consultores Avanzados | N artefactos .lean verificados + reranker |
11. Entrenamiento
`ash
Preparar datos
python scripts/prepare_training_data.py
Fase 1: supervisado (~20 min en RTX 3050)
python scripts/train_gnn_ppo.py --epochs 10 --batch-size 256
Fase 2: PPO con Lean real
python scripts/train_gnn_ppo.py --resume --with-lean --lean-samples 300 --epochs 0 --ppo-epochs 5
Sembrar memoria procedimental (2,371 patrones)
python scripts/seed_from_datasets.py
Entrenar los 14 join-envoltorios especializados
python scripts/train_multiagent.py --epochs 5 `
12. Estructura del Repositorio
Metamatematico/ ├── app.py # App Streamlit ├── nucleo/ # NLE (~13,500 LOC) │ ├── core.py # Orquestador principal │ ├── multi_agent/ # 19 join-envoltorios │ │ ├── orchestrator.py # L3: Orchestrator │ │ ├── colimit_agents.py # L2: 14 join-envoltorios + domain_tactic │ │ ├── pillar_agents.py # L1: 4 PillarAgents │ │ └── mes_bridge.py # Convergencia → extensión del grafo │ ├── graph/ # Grafo categórico │ │ ├── category.py # SkillCategory + morfismos │ │ ├── evolution.py # Extensión, snapshots, functores │ │ └── math_domains.py # 76 skills en 14 categorías │ ├── mes/ # Memory Evolutive Systems │ │ ├── patterns.py # is_join(), propiedad universal │ │ ├── memory.py # Memoria procedimental │ │ └── co_regulators.py # 4 Co-reguladores │ ├── rl/ # Aprendizaje por refuerzo │ │ ├── agent.py # NucleoAgent: PPO + GAE │ │ ├── gnn.py # SkillGNN: 3× GATConv │ │ └── networks.py # ActorCriticNetwork (546K params) │ └── lean/ # Verificación formal │ ├── client.py # LeanClient (subprocess) │ ├── solver_cascade.py # GoalAnalyzer + SolverCascade │ └── sorry_filler.py # SorryFiller + skip_cascade ├── MetamathProver/ # Pruebas Lean 4 verificadas │ ├── ColimitVerifier.lean # Soundness + completeness │ └── JoinColimit.lean # IsJoin ↔ prop. universal, 0 sorry ├── scripts/ # Entrenamiento y utilidades ├── tests/ # 382 tests en 18 suites └── docs/ # Paper NLE v7.0
13. Instalación
`ash git clone https://github.com/metamatematico/Metamatematico---Razonamiento-Formal-con-Lean.git cd Metamatematico---Razonamiento-Formal-con-Lean
conda create -n metamat python=3.10 conda activate metamat pip install -r requirements.txt `
Lean 4 + Mathlib
ash curl https://elan.lean-lang.org/elan-init.sh -sSf | sh lake update # descarga Mathlib (~20-30 min la primera vez)
Sin Lean instalado el sistema funciona completo excepto la verificación formal.
Lanzar
ash PYTHONIOENCODING=utf-8 streamlit run app.py # interfaz web python -m nucleo chat # CLI interactivo
14. Fundamento Teórico
El NLE v7.0 está basado en el artículo "Núcleo Lógico Evolutivo v7.0 — Memory Evolutive Systems y Razonamiento Formal" (Jiménez Martínez, BIOMAT 2025), disponible en docs/NLE_v7_PaperNN.pdf.
Limitaciones honestas
| Reclamo | Estado |
|---|---|
| join[P] es cota superior mínima en G_n | ✓ verificado por is_join() en Python |
| Conexión formal con CategoryTheory.Limits.IsColimit de Mathlib | Trabajo futuro |
| GNN entrenada para selección de tácticas dentro de Lean | Pendiente (actualmente: routing ASSIST/RESPOND) |
| Co-reguladores: analogías Python del formalismo MES categórico | Sin prueba formal completa |
Citación
ibtex @software{metamatematico_nle_v7_2026, author = {Jiménez Martínez, Leonardo}, title = {{Metamatemático NLE v7.0}: Razonamiento Formal con Lean 4, Memory Evolutive Systems y GNN+PPO}, year = {2026}, publisher = {HuggingFace}, url = {https://huggingface.co/metamatematico/Metamatematico}, note = {Sistema completo: https://github.com/metamatematico/Metamatematico---Razonamiento-Formal-con-Lean} }
Leonardo Jiménez Martínez · BIOMAT · Centro de Biomatemáticas · 2026
- Downloads last month
- 139