Explanation Site for AI Proofs / Comparator Guide

I am opening this issue in response to the discussion from #AI authored projects > Searching for Turyn Type Sequences @ 💬.

The intention is to have a guide / site to point to when there are claims of open problems or other extremely long results in Lean, which were written by AI. The Site would mainly focus on Comparator.

Name Idea: Did AI prove it?

Rough Structure Ideas from the top of my head:

• Give a rough explanation of the pitfalls of Lean when it comes to proofs
• Give a introduction to trusted definitions, Mathlib Definitions being the Canonical Example

Introduce Comparator:

• Highest Standard of Verification
• Challenge Module / Solution Module
• Challenge Module should contain the to be trusted definitions
• Small How to Guide (could maybe also be outsourced to Comparator Repo)
• Example Repo / Template

Overlap to https://leanprover-community.github.io/did_you_prove_it.html would have to be considered.

Start by reading the existing did_you_prove_it.html page and the linked discussion, then compare its scope with the proposed Comparator-focused guide. Define the site structure, trusted-definition guidance, challenge and solution module explanation, guide, and example template; done means the proposal resolves overlap with the existing page and specifies a workable site outline.