Ray5th/Lean4-helper

Minimalist UI pass: remove emojis and decorative chrome

Repo cleanup: dead code out, test isolation fix, real README

RAFT-style prompting: distractor-aware framing + usage citations

Retrieval fixes: robust nprobe tuning + goals-only query

Polish UI: labeled controls, depth, live solving feedback

Disable two-stage retry + warn on mid-generation model switch

Fix Groq model IDs against live catalog

Refresh Groq model lineup — drop Llama 3.x/Gemma, add GPT-OSS + friends

Fix UI bugs: bounded panel heights + readable text everywhere

Swap MiniLM retriever for LeanDojo's ByT5 premise encoder

Pin ruff to 0.15.14 and re-sort imports

Add CI/CD: GitHub Actions workflow + ruff config

Add Claude CLI provider for Pro-token billing

benchmark.py: support Claude API + local-files mode

Speed up proof generation: cache components, smaller max_tokens, two-stage retry

Add Claude API support (users supply their own key)

Redesign UI: light Claude.ai-inspired theme

Merge pull request #8 from ray5th/worktree-agent-a0c1e62025fb04462

Merge pull request #7 from ray5th/worktree-agent-a5d6c683e40e73f66

Merge pull request #12 from ray5th/claude/test-scripts-clis

Merge pull request #11 from ray5th/worktree-agent-ab4d84b9b8326f21b

Merge pull request #6 from ray5th/worktree-agent-a4b681bccbbb9eb5f

Merge pull request #15 from ray5th/fuzz/solve-proof-corpus

Merge pull request #5 from ray5th/claude/festive-bouman-4a86a7

Fix 4 bugs found in manual code review

Fix 4 bugs found by stress-test agents + add fuzz/concurrent test suites

Add unit tests for run_agent and build_index CLIs

Add unit tests for ProofAgent wrapper

Add pre-built Mathlib FAISS index (118,885 declarations)

Gracefully skip RAG when FAISS index is missing

Fix stdout race in solve_proof under concurrent requests

Fuzz retriever query handling (fix missing input guards)

Fuzz state machine + fix empty-LLM-output bug

Add parse tests for every problems/*.lean file

Redesign UI as two-pane VSCode-style editor

Redesign Gradio UI with VSCode-style Claude theme

Remove Lean+Mathlib warmup step from Dockerfile

Add missing langchain-huggingface and langchain-classic packages

Fix Dockerfile: collapse multi-line python -c into single line

Fix HF Spaces colorFrom value (orange not in allowed list)

Add Hugging Face Spaces YAML frontmatter to README

Fix Vercel CI: serve static redirect page instead of Python function

Add Hugging Face Spaces deployment with Groq API

Merge pull request #4 from ray5th/claude/intelligent-varahamihira-81b22c

Resolve merge conflicts with main, keeping improved versions

Add MiniF2F benchmark harness and improve proof agent robustness

Fix LLM hallucinated imports and slow thinking mode (#3)

Fix LLM hallucinated imports and slow thinking mode (#2)

Fix LLM hallucinated imports and slow thinking mode

Fix import paths and Mathlib auto-detection for LangChain 1.x