Fermat: Framework for Reasoning and Automated Mathematical Exploration

Fermat is a framework for automated mathematical discovery, designed to explore and discover mathematical concepts and theorems programmatically.

Fermat sports an environment for automated mathematical theory formation. The state space is captured by KnowledgeGraph, a directed graph which stores definitions, conjectures, and theorems. Construction actions in the environment are captured through our production rules in frame/productions which input definitions to create new definitions and conjectures. Our proving tool is currently implemented through Z3. Fermat currently supports exploration in elementary number theory & finite fields.

Installation

Clone the repository and install the required dependencies:

git clone https://github.com/yourusername/FRAME.git
cd FRAME
pip install -r requirements.txt

Setup

API Keys

Fermat experiments use OpenAI's API for generating interestingness functions. You need to set up your API keys:

1. Create a secrets directory in the root of the project (at the same level as the frame directory)
2. Create a file called openai.key in the secrets directory
3. Add your OpenAI API key to the file (just the key, no quotes or other formatting)

Generating Documentation

1. Generated API Documentation: We used sphinx-apidoc to automatically generate RST files for all your Python modules.

2. Built the Documentation: We built the HTML documentation using the make html command.

3. Created a Script: We created a generate_docs.sh script to make it easy to regenerate the documentation in the future.

How to Use the Documentation

1. View the Documentation: Open docs/build/html/index.html in your web browser to view the documentation.

2. Regenerate the Documentation: When you make changes to the codebase, run ./generate_docs.sh from the docs directory to regenerate the documentation.

3. Serving the Documentation: When you want to serve the documentation, run ./serve_docs.sh from the docs directory to serve the generated documentation.

What's Included in the Documentation

• Module Documentation: Documentation for all your Python modules, including classes, functions, and variables.
• Class Hierarchy: Inheritance diagrams for your classes.
• Search Functionality: A search feature to find specific items in your documentation.
• Cross-References: Links between related items in your documentation.

Usage

Basic usage:

from src.theory_builder import TheoryBuilder

# Initialize the builder
builder = TheoryBuilder()

# Add some seed concepts
# ... add your initial concepts ...

# Start exploration
builder.explore()

Mathematical Discovery REPL

Fermat includes a REPL (Read-Eval-Print Loop) interface for interactive mathematical discovery. The REPL allows you to explore mathematical concepts, apply production rules, and discover new mathematical relationships.

Starting the REPL

To start the REPL, run:

python -m frame.repl

Basic Commands

• help: Display available commands and their descriptions
• list concepts: Show all available mathematical concepts
• list rules: Display available production rules
• list conjectures: Show discovered conjectures
• inspect <entity>: Show detailed information about a concept or conjecture
• apply <rule> <inputs...>: Apply a production rule to create new concepts/conjectures
• rename <old> <new>: Rename an entity
• visualize: Create a visualization of the current knowledge graph
• clear: Clear the screen
• exit: Exit the REPL

Example Session

math> list concepts
# Shows available concepts like zero, successor, etc.

math> inspect zero
# Displays detailed information about the zero concept

math> apply specialize successor zero
# Creates a new concept by specializing successor with zero

math> list conjectures
# Shows any conjectures that have been discovered