Problem 6 from IMO 1988

Stream: IMO-grand-challenge

[Michail Karatarakis]

Hi, has Problem 6 from the IMO 1988 been formalised in Lean ?

Let $(q,a,b)$ be a positive integer solution to

$q(ab+1) = a^2 + b^2.$

Show that $q$ is a square.

[Johan Commelin]

ls archive/imo/imo1988_q6.lean

[Michail Karatarakis]

Great, thank you :)