Стремление к строгости в математике имеет долгую и неоднозначную историю — историю, из которой математики могут извлечь уроки сейчас, когда формализуют математику в программе Lean.
Рубрика «доказательство теорем»
Проект Lean: Можно ли формализовать всю математику на компьютере – и нужно ли?
2026-06-26 в 9:36, admin, рубрики: lean, доказательство теорем, история математики, математическая строгость, теорема ферма, формализация математики, формальная верификацияКак в Индиане чуть не узаконили π = 3.2
2023-04-15 в 12:50, admin, рубрики: Биографии гиков, доказательство теорем, закон, индиана, математика, мракобесие, Научно-популярное, число пи, эдвард гудвинПоздравляю всех с (прошедшим) днем числа Пи! (день числа Пи отмечается 14 марта, поскольку эта дата в американском формате записывается в как 3.14 - прим. перев.) Чтобы отметить его как следует, я хочу ненадолго отвлечься от программного обеспечения и поговорить о чем-то особом. Возможно, вы слышали байку о том, как в штате Индиана пытались законодательно приравнять число Пи к чем-то типа 3, или 4, или 3.15. Обычно ее рассказывают в качестве доказательства того, что жители Индианы - бестолковая деревенщина, но это далеко не вся история. Зачем они пытались поменять значение π и на что они рассчитывали?
Пролог – декларативный язык, способный решать любые ребусы и доказывать теоремы
2015-03-26 в 16:22, admin, рубрики: Prolog, доказательство теорем, искусственный интеллект, логическое программирование, математика, Программирование, метки: доказательство теорем, логическое программированиеПредставьте себе высокоуровневый язык, в котором не нужно указывать КАК получить результат, вместо этого нужно просто указать ЧТО вы хотите получить. При этом область применения языка не ограничена и язык способен решать те же задачи, что и любой другой высокоуровневый язык, наподобие JAVA. Кажется фантастикой, не правда ли? Однако такой язык есть и называется он PROLOG. Посмотрим как PROLOG справляется с этой задачей на примере загадывания прологу некоторых загадок и попросим PROLOG выдать доказательство теоремы.
