Here is a first proof-of-concept demonstration of an actual outcome for the erdosproblems/OEIS linkage project. There are a number of Erdos problems relating to irrationality of specific series. I asked an AI to compute several of these series to several decimal places (chatgpt.com/share/68b7160a-3d4), then entered in these decimal strings into the OEIS search bar. I found several hits, which I then uploaded to the project github.com/teorth/erdosproblem .

In particular, I linked Erdos problem 259 erdosproblems.com/259 to OEIS A371134 oeis.org/A371134. In the latter page, there was a reference to a solution to the problem by Chen and Ruzsa doi.org/10.1023/A:1004742930674 that was not known to the erdosproblems.com site. So now we can mark that problem as solved!

I think this type of semi-automated literature search could be a good use case for AI tooling, since the (potentially unreliable) output of such AI tools is only used to locate more reliable human-generated resources, rather than being directly incorporated into the final product.

0
0
0

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/tao/statuses/115135610687969581 on your instance and quote it. (Note that quoting is not supported in Mastodon.)