Companion Generation #18

New Issue

aniva · 2023-10-06T16:30:53-07:00

aniva commented

2023-10-06 16:30:53 -07:00

This is something the 0.2.4 proof system did not support. Suppose we create a hole of this type:

def some_theorem: Σ' p: Prop, p :=
  PSigma.mk _ _

The two holes here would have entangled types, and most importantly the value of one affects the value of the other.

This makes it impossible to fill the two holes independently. Another example would be (credit to Kolomatskaia, A.):

example : ∃ x: Nat, x + 5 = 10 :=
  ⟨_, _⟩

This can be proven by

example : ∃ x: Nat, x + 5 = 10 :=
  have h: 2 + 5 = 10 := by calc
  ⟨_, h⟩

The holes have the types

?m1: Nat
?m2: ?m1 + 5 = 10

This is critical for theorem proving and problem generation and is not something the current system can workaround with. I don't think even LeanDojo can solve it.

This is something the 0.2.4 proof system did not support. Suppose we create a hole of this type: ```lean def some_theorem: Σ' p: Prop, p := PSigma.mk _ _ ``` The two holes here would have entangled types, and most importantly the value of one affects the value of the other. This makes it impossible to fill the two holes independently. Another example would be (credit to Kolomatskaia, A.): ```lean example : ∃ x: Nat, x + 5 = 10 := ⟨_, _⟩ ``` This can be proven by ```lean example : ∃ x: Nat, x + 5 = 10 := have h: 2 + 5 = 10 := by calc ⟨_, h⟩ ``` The holes have the types ```lean ?m1: Nat ?m2: ?m1 + 5 = 10 ``` This is critical for theorem proving and problem generation and is not something the current system can workaround with. I don't think even LeanDojo can solve it.

aniva added this to the 0.2.6 milestone 2023-10-06 16:30:53 -07:00

aniva added the

category

feature

part/Goal

labels 2023-10-06 16:30:53 -07:00

aniva self-assigned this 2023-10-06 16:30:53 -07:00

aniva commented

2023-10-06 16:31:26 -07:00

Pushing back the 0.3 milestone by 20 days due to this problem and library definition readings.

aniva referenced this issue

2023-10-07 16:11:54 -07:00