.env.example

# Main backend setup
# OpenAI / Codex OAuth is the default backend.
# Set MATHCODE_USE_OPENAI=0 to disable it and use an Anthropic backend instead.

# OpenAI / Codex OAuth (default, enabled unless set to 0)
# 1. Run `codex auth login`
# MATHCODE_USE_OPENAI=1
OPENAI_MODEL=gpt-5.4
OPENAI_SMALL_MODEL=gpt-5.4
OPENAI_REASONING_EFFORT=medium

# AUTOLEAN codex backend (default, enabled unless set to 0)
# AUTOLEAN_USE_CODEX=1
AUTOLEAN_CODEX_MODEL=gpt-5.4

# To use the Anthropic API instead of Codex:
# 1. Set MATHCODE_USE_OPENAI=0
# 2. Set ANTHROPIC_API_KEY
# MATHCODE_USE_OPENAI=0
# ANTHROPIC_API_KEY=sk-ant-...
# ANTHROPIC_MODEL=claude-sonnet-4-5

# AWS Bedrock
# Requires MATHCODE_USE_OPENAI=0 and MATHCODE_USE_BEDROCK=1
# MATHCODE_USE_BEDROCK=1
# AWS_REGION=us-east-1
# ANTHROPIC_MODEL=anthropic.claude-sonnet-4-5-20250929-v1:0

# Google Vertex AI
# Requires MATHCODE_USE_OPENAI=0 and MATHCODE_USE_VERTEX=1
# MATHCODE_USE_VERTEX=1
# ANTHROPIC_VERTEX_PROJECT_ID=your-gcp-project
# CLOUD_ML_REGION=us-east5
# ANTHROPIC_MODEL=claude-sonnet-4-5@20250929

# Azure Foundry
# Requires MATHCODE_USE_OPENAI=0 and MATHCODE_USE_FOUNDRY=1
# MATHCODE_USE_FOUNDRY=1
# ANTHROPIC_FOUNDRY_RESOURCE=your-foundry-resource
# ANTHROPIC_MODEL=claude-sonnet-4-5

# MiniMax gateway (Anthropic-compatible)
# Requires MATHCODE_USE_OPENAI=0
# MINIMAX=your_minimax_token
# ANTHROPIC_BASE_URL=https://api.minimaxi.com/anthropic
# ANTHROPIC_MODEL=MiniMax-M2.7
# ANTHROPIC_DEFAULT_SONNET_MODEL=MiniMax-M2.7
# ANTHROPIC_DEFAULT_HAIKU_MODEL=MiniMax-M2.7
# ANTHROPIC_DEFAULT_OPUS_MODEL=MiniMax-M2.7
# Note: MINIMAX is auto-mapped to ANTHROPIC_AUTH_TOKEN at startup.

# Important:
# - Shell-exported env vars override `.env`

# Bundled math tooling defaults to the repo-local AUTOLEAN checkout and Lean workspace.
# Leave these unset unless you explicitly want to override them.
# AUTOLEAN_DIR=/absolute/path/to/AUTOLEAN
# LEAN_PROJECT_DIR=/absolute/path/to/lean-workspace
# MATHCODE_CLI_CMD="/absolute/path/to/bin/mathcode -p"

# Math workflow tuning (optional)
# MATHCODE_MAX_FORMALIZE_ITERS=6        # Formalization compile-repair iterations (default: 6)
# MATHCODE_ATTEMPTS_BEFORE_REPLAN=5     # Proof attempts before replanning (default: 5)
# MATHCODE_MAX_PLAN_ROUNDS=2            # Maximum replanning rounds (default: 2)
# MATHCODE_PROVE_WORKERS=1              # Parallel proof workers across files (default: 1)
# MATHCODE_LSP_TIMEOUT_S=120            # Per-operation LSP timeout in seconds

# Lean LSP — smarter lemma search and structured error feedback during proving
MATHCODE_USE_LSP=1

# Agent-mode proving — full interactive sessions that iteratively prove theorems
MATHCODE_AGENT_PROVE=1
# MATHCODE_AGENT_SESSION_TIMEOUT=600    # Seconds per agent session (default: 600)
# MATHCODE_AGENT_MAX_COMPILES=10        # Max compile attempts per session (default: 10)
# MATHCODE_NUM_PLANNERS=1               # Parallel planners per round (default: 1)

# Tree-of-subgoals proving (DSP-V2-style decomposition) — planner produces a
# Lean skeleton with `have ... := by sorry` steps, each leaf is proved
# independently in parallel, then stitched back together. Falls back to flat
# proving on any failure. Each successful subgoal becomes a first-class
# entry in the lemma cache and a node in the Obsidian vault graph.
# MATHCODE_TREE_PROVE=1
# MATHCODE_MAX_TREE_DEPTH=1              # Max recursion depth (default: 1; leaves proved flat)
# MATHCODE_MAX_DECOMPOSE_RETRIES=3       # Max decomposer attempts to produce a compilable skeleton (default: 3)
# MATHCODE_TREE_LEAF_ATTEMPTS=3          # attempts_before_replan for each leaf subgoal (default: 3)
# MATHCODE_TREE_LEAF_PLAN_ROUNDS=1       # max_plan_rounds for each leaf subgoal (default: 1)
# MATHCODE_PROVE_WORKERS=4               # Parallelism cap for leaf dispatch (also caps cross-problem workers)

# Plan/guide mode — when enabled, AutoLeanProveTool exposes a `planner_guidance`
# input field. The MathCode CLI agent (Claude) is told to distill any strategic
# context from its conversation with the user — explicit hints, agent-side
# analysis, jointly-developed plans, identified key lemmas — into that field.
# The guidance is then forwarded to the planner LLM and injected into every
# per-theorem planner prompt as authoritative context, with the planner
# instructed to focus on parts relevant to the current theorem. Capped at
# 8000 characters. Off by default; flip to 1 to enable.
# MATHCODE_PLAN_GUIDE=1
# Theorem library mode — when enabled, every successfully-proved top-level
# theorem is appended to the active vault's TheoremLib/Stored.lean and
# mirrored into the workspace under VaultLibs/<VaultName>TheoremLib/. Future
# proofs can `import <VaultName>TheoremLib.Stored` and reuse stored theorems
# directly via `exact <VaultName>TheoremLib.<theorem_name> <args>`.
#
# The vault namespace is derived from `basename(MATHCODE_OBSIDIAN_VAULT)` per
# the rule documented in PROJECT.md (PascalCase, with the literal suffix
# `TheoremLib`). MATHCODE_VAULT_NAME bypasses the derivation entirely.
#
# Toggle via the /theorem-store slash command (on/off/sync/status), which
# does the line-level edit of this file for you.
# MATHCODE_THEOREM_STORE=1
# MATHCODE_VAULT_NAME=MyCustomNamespace  # Optional explicit namespace override

# Declaration library — /axiomatize stores persistent, compile-checked
# Lean declarations per-vault. Supports axiom (assumptions), def
# (computable), structure, inductive, abbrev. All domains: math,
# physics, chemistry, narrative, general. Declarations are injected
# into planner prompts as an === ACTIVE DECLARATIONS === section.
# Use `/axiomatize` to manage declarations interactively.
# MATHCODE_AXIOM_AUTO=1              # Auto-detect assumptions in conversation

# Persistent Lean REPL — keeps a Lean LSP server alive with Mathlib
# cached in memory. After ~90s warmup, every compile check takes
# ~0.1-0.5s instead of ~90s. Shared environment includes Mathlib +
# current vault's TheoremLib + AxiomLib. Requires leanclient package.
# MATHCODE_LEAN_REPL=1

API_TIMEOUT_MS=3000000
MATHCODE_DISABLE_NONESSENTIAL_TRAFFIC=1
DISABLE_TELEMETRY=1