Nanomachines, son!
Давненько я не писал ничего про нанотехнологии, но сегодня у нас на повестке дня куда более обширная тема — а что мы не знаем, но уже можем хотеть знать? Если брать физику — да тут куда не дернись, везде стены. И даже если что‑то начинает работать с учетом постулатов или еще каких костылей, то при копке поглубже обязательно уткнешься в очередной спин, который вроде и понятный, но что это и откуда не известно до сих пор.
Пример расчётного доказательства в программе Lean
Математики давно используют компьютеры в своей работе как инструменты для сложных вычислений и выполнения рутинных операций перебора. Например, в 1976 году методом компьютерного перебора была доказана теорема о четырёх красках. Это была первая крупная теорема, доказанная с помощью компьютера.
Теперь вспомогательный софт для доказательства теорем (proof assistant software) не просто проверяет доказательства, но помогает выйти на принципиально новый уровень великого объединения разных математических разделов. Концепция «конденсированной математики» обещает принести новые идеи и связи между областями, начиная от геометрии и заканчивая теорией чисел. Это в своём роде «великое объединение» математики
Читать полностью »
