Obrigado Ruy.
Tenho usado uma versão gratuita do GPT4 através do sincode.ai, me parece
que o Terry Tao está absolutamente correto.
Quando integrado com ferramentas como verificadores de prova, assistentes
de prova como Coq e Isabelle, pesquisa na internet e pacotes matemáticos
simbólicos como
“The 2023-level AI can already generate suggestive hints and promising leads to
a working mathematician and participate actively in the decision-making
process. When integrated with tools such as formal proof verifiers, internet
search, and symbolic math packages, I expect, say, 2026-level AI, w
