Commit 2020-10-13 03:48 505b969c
View on Github →feat(archive/imo): formalize IMO 1962 problem Q1 (#4450) The problem statement: Find the smallest natural number $n$ which has the following properties: (a) Its decimal representation has 6 as the last digit. (b) If the last digit 6 is erased and placed in front of the remaining digits, the resulting number is four times as large as the original number $n$. This is a proof that 153846 is the smallest member of the set satisfying these conditions.