Теорема о четырёх красках и революция в вычислительной математике: 100-летняя задача и философия машинного доказательства
