feat: add hardest theorems from LeanTriathlon

[BoltonBailey]

This PR adds the hardest entries from LeanTriathlon. I found these by asking for an estimate from Claude of the number of informal pages of math to prove: These are the only theorems in LeanTriathlon which are

• Not already in lean-eval in some form
• Take more ~pages than Thue-Siegel-Roth theorem and Mergelyan's theorem, which appear both in lean-eval and LeanTriathlon and which have already been solved on the lean-eval leaderboard.

So perhaps these are the theorems that give us a good chance of distinguishing ultra-powerful models. The theorems are:

• Friedlander–Iwaniec theorem. "There are infinitely many primes of the form a² + b⁴."
• Duffin–Schaeffer Conjecture / Koukoulopoulos–Maynard theorem on rational approximability.
• Linnik's theorem on the least prime in an arithmetic progression. (In the interest of maximizing difficulty, I made the constant explicit.)
• The Bhargava-Hanke 290 theorem on integral quadratic forms.

Perhaps the Friedlander-Iwaniec theorem could have been replaced by the later a^3 + 2b^3 Heath-Brown result which is said to be similar, but it seems less well known, and I am ultimately not sure it is more difficult.

I have done my best to present some outlines of the formal proofs for these, but these are theorems with really long proofs, hard to summarize. In the case of the Koukoulopoulos-Maynard theorem, there does not really seem to be a succinct description of their approach in their paper or elsewhere on the internet, so I left it blank.

Depends on #467 for a fix to the repo health check procedure.