mathcode/.env.example at main · math-ai-org/mathcode · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
# 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

# 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
# CLAUDE_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)

API_TIMEOUT_MS=3000000
MATHCODE_DISABLE_NONESSENTIAL_TRAFFIC=1
DISABLE_TELEMETRY=1