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 wi

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 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).