.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.5
OPENAI_SMALL_MODEL=gpt-5.5
OPENAI_REASONING_EFFORT=high

# OpenRouter via the OpenAI-compatible Responses API
# Requires MATHCODE_USE_OPENAI=0 and MATHCODE_USE_OPENROUTER=1
# MATHCODE_USE_OPENROUTER=1
# OPENROUTER_API_KEY=sk-or-...
# OPENROUTER_MODEL=openai/gpt-5.5
# OPENROUTER_SMALL_MODEL=openai/gpt-5.5
# OPENROUTER_REASONING_EFFORT=high
# OPENROUTER_BASE_URL=https://openrouter.ai/api/v1
# Optional attribution headers:
# OPENROUTER_HTTP_REFERER=https://your-app.example
# OPENROUTER_APP_TITLE=MathCode
#
# Alternative OpenAI-compatible gateway: Atlas Cloud
# Use the same OpenRouter route, but set OPENROUTER_API_KEY to your Atlas key,
# set OPENROUTER_BASE_URL to https://api.atlascloud.ai/v1, and set
# OPENROUTER_MODEL to deepseek-ai/deepseek-v4-pro or another live Atlas model.
# https://www.atlascloud.ai/?utm_source=github&utm_medium=link&utm_campaign=mathcode

# AUTOLEAN codex backend (default, enabled unless set to 0)
# AUTOLEAN_USE_CODEX=1                            # legacy global toggle; AUTOLEAN_BACKEND below supersedes
AUTOLEAN_CODEX_MODEL=gpt-5.5                      # leave empty ("") to use codex's own config default

# Per-stage backend routing (all optional).
# Each AUTOLEAN_*_BACKEND accepts: codex | cli | openrouter.
# Unset stages inherit AUTOLEAN_BACKEND (default: codex).
# Each AUTOLEAN_*_MODEL is only consulted when its stage is openrouter;
# codex stages always use AUTOLEAN_CODEX_MODEL; cli stages use whatever the
# main mathcode CLI is configured for.
#
# Legacy vars still honored as fallbacks when the new ones are unset:
#   AUTOLEAN_BACKEND                      <- AUTOLEAN_USE_CODEX
#   AUTOLEAN_FORMALIZE_PLAN_BACKEND       <- AUTOLEAN_THINKING_USE_CODEX
#   AUTOLEAN_FORMALIZE_BACKEND            <- AUTOLEAN_CODING_USE_CODEX
#   AUTOLEAN_FORMALIZE_EVAL_BACKEND       <- AUTOLEAN_EVAL_USE_CODEX
#   AUTOLEAN_PROVE_PLAN_BACKEND           <- AUTOLEAN_PLANNER_USE_CODEX
#   AUTOLEAN_PROVE_BACKEND                <- AUTOLEAN_PROVER_USE_CODEX
#   AUTOLEAN_FORMALIZE_PLAN_MODEL         <- AUTOLEAN_OPENROUTER_THINKING_MODEL
#   AUTOLEAN_FORMALIZE_MODEL              <- AUTOLEAN_OPENROUTER_MODEL
#   AUTOLEAN_FORMALIZE_EVAL_MODEL         <- AUTOLEAN_OPENROUTER_EVAL_MODEL
#   AUTOLEAN_PROVE_PLAN_MODEL             <- AUTOLEAN_PLANNER_MODEL
#   AUTOLEAN_PROVE_MODEL                  <- AUTOLEAN_PROVER_MODEL
#
# Example: keep planning stages on codex, route Lean-output stages to
# OpenRouter + Gemini 3 Flash:
# AUTOLEAN_BACKEND=codex
# AUTOLEAN_FORMALIZE_BACKEND=openrouter
# AUTOLEAN_FORMALIZE_MODEL=google/gemini-3-flash-preview
# AUTOLEAN_PROVE_BACKEND=openrouter
# AUTOLEAN_PROVE_MODEL=google/gemini-3-flash-preview
# OPENROUTER_API_KEY=sk-or-...
#
# AUTOLEAN_BACKEND=codex
# AUTOLEAN_FORMALIZE_PLAN_BACKEND=codex
# AUTOLEAN_FORMALIZE_PLAN_MODEL=
# AUTOLEAN_FORMALIZE_BACKEND=codex
# AUTOLEAN_FORMALIZE_MODEL=
# AUTOLEAN_FORMALIZE_EVAL_BACKEND=codex
# AUTOLEAN_FORMALIZE_EVAL_MODEL=
# AUTOLEAN_PROVE_PLAN_BACKEND=codex               # also used for the tree decomposer
# AUTOLEAN_PROVE_PLAN_MODEL=
# AUTOLEAN_PROVE_BACKEND=codex
# AUTOLEAN_PROVE_MODEL=

# 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

# Prefix-cache request-shape diagnostics and policy controls.
# MathCode does not emit model-visible prompt-header attribution for any
# provider route. Provider-native cache fields remain governed by cache policy.
# MATHCODE_DISABLE_CACHE_STABLE_PROMPTS=1
# MATHCODE_DISABLE_CACHE_POLICY=1
# MATHCODE_CACHE_MULTI_BREAKPOINT=1
# MATHCODE_CACHE_EXPLICIT_MIN_PREFIX_GATE=1
# MATHCODE_CACHE_TTL_IDLE_AWARE=1
# MATHCODE_CACHE_TTL_IDLE_THRESHOLD_MS=300000
# MATHCODE_DISABLE_TOOL_CANONICALIZATION=1
# MATHCODE_DISABLE_BETA_CANONICALIZATION=1

# 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 Lean workspace.
# Leave these unset unless you explicitly want to override them.
# 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
# MATHCODE_GOAL_MAX_TOKEN_BUDGET=1000000000  # Source/WebUI goal token-budget ceiling (also accepts integer-valued decimals and k/m/b suffixes)
# MATHCODE_MAX_CHAINED_COMMAND_INPUTS=25     # Nested local slash-command next-input ceiling

# Kimina Lean Server — external long-lived Lean compiler service (see
# https://github.com/project-numina/kimina-lean-server). When enabled,
# mathcode spawns the server as a subprocess at startup, keeps it alive
# until mathcode exits, and routes every Lean compile check through its
# HTTP /verify endpoint. Preempts the in-process Lean REPL when ready;
# falls through to the REPL (then `lake env lean`) otherwise.
# MATHCODE_KIMINA_SERVER=1
# MATHCODE_KIMINA_CMD="python -m server"          # required; how to start the server
# MATHCODE_KIMINA_CWD=/absolute/path/to/kimina-lean-server   # cwd for the start command (default: $PWD)
# MATHCODE_KIMINA_PORT=12332                      # port the server listens on (default: 12332, matches kimina)
# MATHCODE_KIMINA_STARTUP_TIMEOUT_S=300           # how long to wait for the server to answer /verify

# 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 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)` using
# the repository's theorem-library rule (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. Built in; no separate install required.
# MATHCODE_LEAN_REPL=1

API_TIMEOUT_MS=3000000
MATHCODE_DISABLE_NONESSENTIAL_TRAFFIC=1
DISABLE_TELEMETRY=1