итс май лайф

Интересно, кто-нибудь пробовал массово переводить хорошо известную математику в формальный вид для программ типа Coq или Agda? Это интересная идея для проекта — я хоть и далек уже от математики, но и мне было бы забавно почитать и порефакторить получившийся код.

Update: нашел IsarMathLib и Metamath, читаю. В гугле надо искать "formalized mathematics", попадаются интересные находки вроде этой.

Я научился представлять себе звучание двух нот одновременно. Не каждый день и не очень четко, но иногда у меня определенно получается.

Погрузитесь в долбанутый мир электронной музыки! Осторожно, можно полчаса просидеть прокликать.

Когда больше года подряд каждое утро за стеной кто-то сверлит, это вызывает не только раздражение, но и любопытство.

Чудесная флеш-игрушка Windosill.

Несколько вопросов, на которые биология пока не знает хорошего ответа: чем выгодно существование полов, зачем нужен сон, как происходит старение, что такое самосознание, как зародилась жизнь.

Придумал классную мелодию, напел ее на мобильник и забыл. Через три часа послушал и ни хрена в ней не понимаю. Но если повторить десять раз, то какое-то смутное понимание начинает прощупываться. Мда.

I just pity anybody who's gotta buy a fantasy from somebody else or get it from a computer. How pitiful can you get, you can't even dream your own dreams for god sake?

У Оруэлла мелькает идея, что самый адекватный способ перевода на новояз — это "идеологический перевод" с изменением смысла, например тексты о демократии превращаются в восхваление абсолютной власти.

Я попытался идейно перевести на русский язык известную цитату Вольтера: "Я не согласен с тем, что вы говорите, но готов умереть за ваше право это говорить."

Получилось вот что: "Я согласен с тобой по сути, но готов умереть убить тебя, чтобы ты не высказывал это в такой форме."

*спасибо ivanoff272 за исправление

Я понял, как в русском языке чаще всего выражается магическое мышление: как вера в симпатическую магию слов — убеждение других с помощью эскалации завораживающе расширяющихся понятий вроде "должен", "гнусно", "друг" или "мать", или долгие раздумья о глубинной правде формулировок в услышанной где-то меткой фразе с надеждой в будущем руководствоваться ей и сделать свою жизнь правильнее. Если мастерски овладеть этой магией, не теряя искренней веры в нее, то можно принудить самого себя или других русских к чему угодно. Но я убежден, что каждому из нас по отдельности было бы лучше никогда ей не пользоваться и не поддаваться.

Чувство глубинной правды не дает тебе гарантий, что следование ей приведет тебя к лучшей жизни. А если правда мелкая и выражена узкими неметафоричными словами с обычной логикой, то никаких гарантий не надо, можно просто проверить. Хотя плоский способ мышления непривычен и требует тренировки, особенно если ты начитался русской литературы или часто общаешься с родственниками.

Усилия по тренировке музыкального слуха принесли плоды: к моим ушам стали приставать случайно услышанные музыкальные отрывки. Раньше я завидовал чужим рассказам об этой напасти, а теперь понимаю их жалобы.

Терри Прэтчетт объясняет, как из Эвереттовской интерпретации квантовой механики следует существование рая и ада. Пол Олмонд объясняет, как из нее же следует простое решение парадокса Ферми. А если кто-то сомневается в множественности миров, вот эксперимент, который ее доказывает.

Придумал простое изложение Simpson's paradox. Предположим, что:

1) Большинство женщин выживает после некой болезни, а большинство мужчин умирает.

2) Большинство женщин принимает некое лекарство, а большинство мужчин не принимает.

3) Лекарство не влияет на вероятность выживания, т.е. не действует ни хрена. Разница в выживаемости объясняется физиологическими различиями мужчин и женщин, а разница в приеме лекарства - различиями психологическими. :-)

Тогда, если при статистическом исследовании вы не догадались посчитать мужчин отдельно и женщин отдельно, то вы придете к выводу, что лекарство приносит пользу. Понятно, что аналогичным трюком (вводом и исключением новых переменных) можно обращать знак статистических зависимостей и вообще по-всякому развлекаться.

Мораль: чтобы выяснить настоящую, а не желаемую причинно-следственную связь между наблюдаемыми переменными, простого наблюдения за закономерностями реального мира недостаточно. Надо проводить слепой эксперимент. Или, если это невозможно (например в социологии), по крайней мере ввести в статистическое вычисление кучу дополнительных "контрольных" переменных, которые взбредут вам в голову. :-)

Я Платон, а ты планктон!

Песенка из моего детства

Очень красивая математическая конструкция: Ford circles.

Научился в уме очищать фразы от слов, употребленных не в буквальном смысле. Результаты интересные.

Социальная реклама в метро: "Любовь к родине начинается с семьи. Ф. Бэкон." Чтобы прояснить эту фразу, попробуем чем-нибудь заменить сомнительное слово "начинается". Первый вариант: фраза информирует читателя о корреляции между любовью к родине и любовью к семье, но тогда непонятно, для чего ее написали на плакате. Второй вариант: фраза маскирует повелительное наклонение. Если хочешь любить родину, сначала люби семью. Обычная тактика убеждения: ты обязан подчиниться логике своих собственных ценностей и сделать то-то.

Если какую-то мысль стыдно высказать вслух, это не повод запрещать себе ее думать.

Программист всегда различает вещь, имя вещи и имя имени вещи лучше любого философа.

Кто-нибудь разбирается в глобальном потеплении? Объясните мне вот это.