Community

Contributing to JuGeo

JuGeo is an ambitious project at the intersection of algebraic geometry, proof theory, and Python verification. We welcome contributions across all areas.

Contribution Areas

📐

Theory & Foundations

Contribute to the mathematical framework. Improve existing proofs, extend the foundations, and develop new theoretical results.

🧪

Lean Proofs

Formalize new theorems in Lean 4. Improve existing proof files. Add lemmas and helper structures.

🐍

Python Implementation

Improve the ~960 module codebase. Add new encodings, improve solver routing, extend the effect system.

🧱

Benchmarks & Tests

Add test cases to the 300+ benchmark suite. Create new experiment scripts. Improve coverage.

📚

Documentation

Improve this documentation site. Write tutorials, add examples, fix errors.

🤖

Copilot Integration

Improve the LLM evidence channel. Better prompt engineering, trust calibration, oracle federation.

Development Setup

bash

git clone https://github.com/thehalleyyoung/jugeo.git
cd jugeo
pip install -e .
pytest test_examples/ -v      # Run tests
python3 test_algorithms.py    # Run algorithm tests

Guidelines

Python ≥ 3.10 — use modern Python features (match statements, type hints, dataclasses)
Frozen dataclasses — core data structures should be immutable
Strict dependency DAG — respect the layer ordering (kernel → geometry → judgments → ...)
Trust is sacred — never allow silent trust promotion in any code path
Evidence is multi-channel — don't collapse different evidence types into a single boolean
Obstructions are first-class — failures should be structured Obstruction objects, not strings

Pull Request Process

Fork the repository and create a feature branch
Ensure all existing tests pass: pytest test_examples/ -v
Add tests for new functionality
If adding theory, consider a corresponding Lean proof in proofs/lean/
Submit a PR with a clear description of what changed and why

Architecture Principles

The Dependency DAG

The ~960 modules follow a strict layered architecture. Lower layers never import from higher layers:

kernel → geometry → judgments → evidence → solver → encodings
  → python_runtime → generation → orchestration → ideation → problem_modes