openai / lean-gym

Apache License 2.0
150 stars 31 forks source link

How to search a customed theorem with lean-gym? #27

Open liebenxj opened 1 year ago

liebenxj commented 1 year ago

Hi, I wonder how to search a customed theorem with lean-gym? For example, ∀ (a b : ℝ), ∃ x, (a + b) ^ 3 = a ^ 3 + x a ^ 2 b + 3 a b ^ 2 + b ^ 3. Thanks!