Re:Terence Tao on GPT-4
by williamstein on Wednesday April 12, 2023 @10:47AM
(#35540642)
I would not discount the potential of LLM's to support research level mathematics. There's interesting research going into combining the LEAN theorem prover with LLMs, e.g., this recent paper: https://arxiv.org/abs/2202.01344
"... automatically solving multiple challenging problems drawn from high school olympiads."
This combination of GPT and LEAN is the first thing that has finally got me really interested in the potential of LEAN. And LEAN very directly addresses the "bullshit" issue, since it formally verifies whether or not a proof is correct (it's like a compiler like Rust, but for mathematical proofs).
"... automatically solving multiple challenging problems drawn from high school olympiads."
This combination of GPT and LEAN is the first thing that has finally got me really interested in the potential of LEAN. And LEAN very directly addresses the "bullshit" issue, since it formally verifies whether or not a proof is correct (it's like a compiler like Rust, but for mathematical proofs).