justinpombrio comments on “AI achieves silver-medal standard solving International Mathematical Olympiad problems”

[justinpombrio]

The feedback is from Lean, which can validate attempted formal proofs.