#meme про детей

TIL, что GitHub ещё и STL умеет рендерить нынче (у меня 3D-принтера нет, так что я как-то это новшество упустил). Узнал о такой функциональности, решив взглянуть, как выглядит результат генерации этих весёлых ёлочных игрушек: https://github.com/joe-warren/christmas-ornaments/blob/main/haskell-ornament.stl

Мальчик: хвастается перед друзьями новой машиной
Мужчина: хвастается перед друзьями новыми джинсами

#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.

В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.

Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.

Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.

Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.

Кевин заключает замечанием о том, в каком хрупком состоянии находится современная математика, сколько критических деталей известны лишь специалистам и нигде толком не прописаны.
--------

Меня в этой истории вдохновляет, что к нам в математику как будто приходит живой трибунал, универсальный калькулятор истинности. Пока утверждение не компилируется Lean'ом, оно не считается доказанным.

Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!

В СМЫСЛЕ НОВЫЙ ГОД НА НОСУ

#meme про... Девушек

jshell> Stream.iterate(1, x -> x * 4 + 1).limit(10).map(Integer::toBinaryString).map(x -> " ".repeat(9 - x.length() / 2) + x).forEach(System.out::println)
         1
        101
       10101
      1010101
     101010101
    10101010101
   1010101010101
  101010101010101
 10101010101010101
1010101010101010101

С Наступающим!

BTW, jshell прям нормальный, выводит типы подвыражений и методы автодополняет :)

ГОВНО С ДЫМОМ

Я нашёл!

В СМЫСЛЕ УЖЕ ЯНВАРЬ

#prog #article

Debugging memory corruption: Who wrote ‘2’ into my stack?!

Статья из 2016 про отладку связанного с сокетами кода Unity на Windows.

TL;DR: в коде Unity для обработки очереди сокетов использовался сисколл select, в реализации которого вызывалась функция, которая записывала статус возврата в переменную на стеке. При добавлении нового сокета нужно было прервать исполнение сисколла, чтобы можно было начать слежение за состоянием нового сокета. В реализации на тот момент использовалось API для добавления пользовательских асинхронных коллбеков на состояния потока. Этот коллбек выбрасывал исключение, что приводило к раскрутке стека. Когда выполнение сисколла завершалось, он записывал статус в стековую переменную, которой больше не было.