A Robbins pentagon is a cyclic pentagon whose edge lengths and area as all rational numbers.
All known Robbins pentagons have rational diagonals, but it has not yet been proven that no Robbins pentagons with irrational diagonals can exist.
Obviously, finding such a pentagon with irrational diagonals would solve this problem. The problem might also be solved by assuming the existence of a smallest primitive integer Robbins pentagon, and then deducing the existence of a smaller such pentagon with integer side lengths, which would be a proof by contradiction.
Has there been any progress? Have any properties of a hypothetical Robbins pentagon with irrational diagonals been proven?