Spaces:

Ray5th
/

Lean4-helper

Running

Lean4-helper / problems /simple_add.lean

p4r5kpftnp-cmd

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

3ac681e about 2 months ago

76 Bytes

	import Mathlib

	theorem add_zero_simple (n : ℕ) : n + 0 = n := by
	sorry