fix(ErdosProblems): Add formalized lean sources to Erdos Problems

[danielchin]

Adding formalized lean sources.

There's a few exceptions that I've caught:

1. 303 was actually written in lean3 and the only category annotation is lean4. Maybe we add a lean3 annotation?
2. The URL for 303 is actually way too long, even for URL shorteners because it's using live.looken.cn. I'm leaving this out for now until we figure how we want to reference it.

Also took the liberty to fix up some of the docstrings and references.

Closes #2334
Closes #2335
Closes #2336
Closes #2337
Closes #2338
Closes #2339
Closes #2340
Closes #2341
Closes #2342
Closes #2343
Closes #2344
Closes #2345
Closes #2346
Closes #2347
Closes #2348
Closes #2349
Closes #2350
Closes #2351
Closes #2352
Closes #2353
Closes #2354
Closes #2355

[mo271]

Adding formalized lean sources.

There's a few exceptions that I've caught:

1. 303 was actually written in lean3 and the only category annotation is lean4. Maybe we add a lean3 annotation?

No, let's just use the FormalProofKind called otherSystem.

2. The URL for 303 is actually way too long, even for URL shorteners because it's using live.looken.cn. I'm leaving this out for now until we figure how we want to reference it.

In this case let's just "link to the link", namely link to https://www.erdosproblems.com/forum/thread/303

Also took the liberty to fix up some of the docstrings and references.

Great!

[mo271]

Thanks, looks great, @danielchin: let's also fix the URL 303 as described in the comment above, otherwise this is good to go!

[danielchin]

Oops, looks like I misspoke, 289 and 299 were the ones that were written in lean3, so updated those to say other_system.