|
|
|
|
|
by pred_
9 days ago
|
|
I guess we won't know if that's what was used (and maybe even provided as part of the prompt given that both Alpöge and Mathew are mathematicians) since they decided against sharing their Fable conversation and instead opted for a memey tweet as their avenue of publication. We really ought to normalize full transparency in how results come about. Anyway, if I read Tao's post and comment correctly, there's still a gap from the Vitushkin construction to a counterexample, but chances are that was in the training data. In general, it is just a serious problem for their practical applicability that the models are outputting proofs with absolutely terribly reference hygiene. |
|
I more and more see LLMs as a kind of scam; not useless, but really just a big database of fuzzy facts with some Prolog on top as rediscovered by the learning algorithm. Most likely could be made much cheaper to run, were humans allowed to actually inspect the algorithm.