Spaces:
Running
Running
p4r5kpftnp-cmd
Add LangChain/LangGraph RAG pipeline for retrieval-augmented proof generation
3ac681e | import Mathlib | |
| theorem square_root_two_irrational (n m : ℕ) (h : n^2 = 2 * m^2) (hm : m ≠ 0) : False := by | |
| sorry | |