Current hopes (even by Terrence Tao) are that you give a sketch of a proof to GPT-X and it will give you a link to the formally confirmed proof. Others hope th

Current hopes (even by Terrence Tao) are that you give a sketch of a proof to GPT-X and it will give you a link to the formally confirmed proof. Others hope that the next AI will come up with a sketch of a proof itself. GPT-4 sucks at lean because lean had it's syntax changed too often, and GPT-4 shows limited reasoning capabilities However it did come up with the following proof for my little order of pairs instance LT : LT (ℕ × ℕ) where lt f g := f.1 < g.1 ∨ (f.1 = g.1 ∧ f.2 < g.2) instance : DecidableRel (LT.lt : ℕ × ℕ → ℕ × ℕ → Prop) := fun (a,b) (c,d) => if h₁ : a < c then isTrue (Or.inl h₁) else if h₂ : a = c then if h₃ : b < d then isTrue (Or.inr ⟨h₂, h₃⟩) -- the rest is even more silly since we have to turn everything around else isFalse (λ (h : a < c ∨ (a = c ∧ b < d)) => Or.elim h (λ hlt : a < c => absurd hlt h₁) (λ heq : a = c ∧ b < d => absurd (And.right heq) h₃)) else isFalse (λ (h : a < c ∨ (a = c ∧ b < d)) => Or.elim h (λ hlt : a < c => absurd hlt h₁) (λ heq : a = c ∧ b < d => absurd (And.left heq) h₂) ) This may lead back to the original question because Bool ≠ Prop and the formula for LT should ideally lead directly to decidability without all this redundancy?