Hugging Face's logo

Spaces:
Ray5th
/
Lean4-helper
Running

App Files Community
Lean4-helper / src

Commit History

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

p4r5kpftnp-cmd commited on

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

p4r5kpftnp-cmd commited on

Retrieval fixes: robust nprobe tuning + goals-only query
1dc8f6a

p4r5kpftnp-cmd commited on

Swap MiniLM retriever for LeanDojo's ByT5 premise encoder
d05440d

p4r5kpftnp-cmd commited on

Pin ruff to 0.15.14 and re-sort imports
01cdf65

p4r5kpftnp-cmd commited on

Add CI/CD: GitHub Actions workflow + ruff config
6cf7e7c

p4r5kpftnp-cmd commited on

Add Claude CLI provider for Pro-token billing
a8eac5b

p4r5kpftnp-cmd commited on

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

p4r5kpftnp-cmd commited on

Add Claude API support (users supply their own key)
1145e92

p4r5kpftnp-cmd commited on

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

Ray5th commited on

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

Ray5th commited on

Fix 4 bugs found in manual code review
1808386

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on

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

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on

Gracefully skip RAG when FAISS index is missing
41f9289

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on

Fuzz retriever query handling (fix missing input guards)
1c701bb

p4r5kpftnp-cmd Claude Opus 4.7 commited on

Fuzz state machine + fix empty-LLM-output bug
ec7552d

p4r5kpftnp-cmd Claude Opus 4.7 commited on

Add Hugging Face Spaces deployment with Groq API
c2ebdf5

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on

Add MiniF2F benchmark harness and improve proof agent robustness
8c51ce7

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on

Fix LLM hallucinated imports and slow thinking mode
ef4afaa

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on

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

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on

Add LangChain/LangGraph RAG pipeline for retrieval-augmented proof generation
3ac681e

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on

rework
4562b5e

p4r5kpftnp-cmd commited on

Initial commit: Agentic Lean 4 Theorem Prover
4a3b0d0

p4r5kpftnp-cmd commited on