Comment by LightMachine

If we want to test these beasts in logic, we should probably start using actual formalized logic, rather than English. In just one test, Gemini flopped hard, while GPT-4-Turbo nailed it. Here is my prompt:

    Below is a well-typed CoC function:

    foo
    : ∀(P: Nat -> *)
      ∀(s: ∀{n} -> ∀(x: (P n)) -> (P (n + 1)))
      ∀(z: (P 0))
      (P 3)
    = λP λs λz
      (s (s (s z)))

    Below is an incomplete CoC function:

    foo
    : ∀(P: Nat -> *)
      ∀(f: ∀{n} -> ∀(x: (P n)) -> (P (n * 3)))
      ∀(g: ∀{n} -> ∀(x: (P n)) -> (P (n * 2)))
      ∀(h: ∀{n} -> ∀(x: (P n)) -> (P (n + 5)))
      ∀(z: (P 1))
      (P 17)
    = λP λf λg λh λz
      {{FILL_HERE}}

    Complete it with the correct replacement for {{FILL_HERE}}.
    Your answer must contain only the correct answer, and nothing else.

- *GPT-4-Turbo answer:* `(f (g (h (g z))))` (correct)

- *Gemini Advanced answer:* `h (h (g (f z)))` (wrong)

Also, Gemini couldn't follow the "answer only with the solution" instruction and provided a bunch of hallucinated justifications. I think we have a winner... (screenshots: https://imgur.com/a/GotG0yF)