HoTT-CatWorld: A Structure-Aware World Model Framework Based on Higher Category Theory

This introduces the core positioning of the HoTT-CatWorld project: integrating world model techniques from machine learning with higher category theory/homotopy type theory (HoTT). Its goal is to achieve verifiable formal reasoning by encoding proof states into high-dimensional graph structures, accelerating the proof search process in the field of higher category theory. This framework is an innovative attempt of neuro-symbolic AI in the field of formal mathematics.

Formal mathematical proof is an important interdisciplinary topic between computer science and mathematics. However, traditional proof assistants (such as Coq and Agda) rely on manual step-by-step writing, which is inefficient and has a high barrier to entry. In recent years, AI for Math has become a hot topic, but most focus on natural language mathematical reasoning. HoTT-CatWorld takes a different approach, focusing on the abstract field of higher category theory, trying to enable AI to understand and manipulate complex mathematical structures. It combines world models (internal representations of the environment by agents in reinforcement learning) with HoTT/higher category theory to solve the problem of proof search efficiency.

• Homotopy Type Theory (HoTT): A combination of type theory and algebraic topology, interpreting type equality as paths in topological spaces, where proof equivalence corresponds to homotopy between paths. Mathematical structures have layers such as objects, 1-morphisms, and 2-morphisms.
• Higher Category Theory: An extension of category theory that allows high-dimensional morphisms (e.g., 2-categories include 2-morphisms between morphisms, and infinity categories have infinitely extending layers), providing a powerful expressive language for complex mathematical relationships.
• World Model: An internal representation of the environment by an agent in reinforcement learning, which enables planning and reasoning by predicting state changes without real environment interaction.

• High-Dimensional Graph State Encoding: Design data structures to represent proof states, including objects (types, terms), morphisms (functions, mappings), 2-cells (morphism transformations/homotopies), paths (equality proofs), diagrams (structural visualization), and consistency (compatibility of high-dimensional structures), allowing neural networks to perceive the topological structure of proofs.
• World Model Architecture: Uses MLP combined with LayerNorm for training, learning to predict the next state under the current proof state + strategy, handling state transitions in high-dimensional graph spaces.
• Verification-Guided Planner: An MCTS-based planner that combines value functions to select strategies, uses the world model to predict state transitions, and ensures the legality of each step through a rule verifier, realizing a hybrid mode of "model prediction + rule verification".

• Strategy Library: Contains 13 strategies covering common operations in higher category theory proofs, such as intro (introduce assumptions), reflexivity (close reflexive equality), apply (apply lemmas), rewrite (rewrite equality), transport (transport along paths), use_segal (apply Segal composition), etc.
• Project Structure: Modular design with folders including core (higher category data structures), state (proof state encoder), model (world model and value function), search (MCTS planner), env (simulated HoTT environment), data (data generation and loading), and examples (sample programs).

• Training Data Sources: Plans to use 1Lab (HoTT/category theory formalization library), agda-unimath (Agda implementation of UniMath), and Rzk proof assistant (infinity category proof tool).
• Usage Methods: Provides command-line tools such as viewing information (hottworld info), running simulations (hottworld simulate --problem path_composition), searching for proofs (hottworld search --problem simple_equality --simulations 50), generating data (hottworld generate --samples 100), and training models (hottworld train --samples 200); sample programs cover classic problems such as path composition and naturality squares.

• Technical Value: Provides new ideas for formal proof automation (data-driven methods to handle complex structures); embodies the concept of neuro-symbolic AI (complementarity between neural network perception and symbolic system reasoning); explores high-dimensional graph structure learning, inspiring the fields of graph neural networks and geometric deep learning.
• Limitations: Currently uses a simulated environment and has not integrated real proof assistants; formalized data for higher category theory is scarce; neural model decisions lack interpretability.
• Future Outlook: Short-term goals include integrating Cubical Agda and Rzk, expanding data scale, improving model accuracy, and developing an interactive interface; the long-term vision is to build an AI assistant that helps mathematicians research higher category theory.