Доказать трансцендентность чисел e и π (Agda2)

http://www.google.ru/search?q=трансцендентность+чисел+e+и+π

а на Agda2 слабо? ;)

Феликс Клейн. «Элементарная математика с точки зрения высшей»

Нафига, если моск справляется?

Забить в Agda2 факт, что e и π трансцендентны - и всё :)

вот это я понимаю - человек без чувства юмора

Нафига, если моск справляется?

не вопрос. тогда усиливаем задание до гипотезы Римана

справишься?

впрочем, можно и доказательство Коэна о независимости аксиомы выбора в ZF

Можно вопрос - Вы на какой специальности учились/учитесь? просто я на прикладной математике, и ничего подобного не помню. Интересно же.

Вы на какой специальности учились

примат я

и ничего подобного не помню

трансцендентные числа и гипотеза Римана - это алгебра и теория чисел, аксиома выбора - теория множеств

Ясно - как и я. И раз этого не было, то ли я плохо учился, то ли тупо этого не давали. Надо наверстывать. Извиняюсь за оффтоп)

Не говоря уж о том, что про такую программу автоматической проверки доказательств вообще впервые слышу. Эх. Там же не логическое программирование используется, а функциональное?

Дальше свойств умножения в Agda2 не дошел. Если запилишь, расшарь.

п.с. Там волне живой мейлинг-лист с суровыми нердами.

Там же не логическое программирование используется, а функциональное?

Изоморфизм Карри-Ховарда используется.

Там же не логическое программирование используется, а функциональное?

система типов Мартина-Лофа там используется. прежде всего

Дальше свойств умножения в Agda2 не дошел. Если запилишь, расшарь.

топик создавался исключительно как пародия. сам я до Agda2 пока не дошёл, только-только начал с Coq разбираться

Там волне живой мейлинг-лист с суровыми нердами.

вот в чём-чём, а в суровости ни разу не сомневался :)

>примат я

А какого учебного заведения?

А какого учебного заведения?

в данный момент - никакого. в прошлом - ДонНУ

Оракулы — это не наш метод! ©

Оракулы — это не наш метод!

именно что!