Тут я знову представляю повну автоматичну формалізацію нещодавньої роботи з математики! Баранчук, Стефан. "Зменшення кількості рівнянь, що визначають підмножину n-простору над скінченним полем." Annales de la Faculté des sciences de Toulouse : Mathématiques,. 6, том 33, No 1 (2024): 177–182. Я провів кілька днів над цим проєктом. Спочатку я провів Арістотеля за @HarmonicMath, який приблизно за 15 годин повністю автоматично формалізував доказ. Потім, завдяки великій допомозі @PietroMonticone, мені вдалося створити креслення пробного матеріалу. Це версія, в якій усі частини документації в LaTeX стають інтерактивними та можуть бути ознайомлені та вивчені. Ми можемо побачити залежності в доведенні та вивчати їхні зв'язки. На етапі постобробки я також використав Grok Heavy і Codex CLI з GPT-5.2 у режимі xhigh для написання покрокового аналізу формального доказу. Це чудова допомога для тих, хто не є професійними програмістами Lean 4. Ви справді можете засвоїти всі етапи доказу. Я хочу підсумувати свої враження та те, чого навчився з цього досвіду. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei

Математичні роботи потребують формальної валідації. Зазвичай це виконується неформально арбітром. Але що, якби ми могли покладатися на щось більш надійне, наприклад, автоформалізацію в Lean 4, де роль рефері зводиться до ретельної перевірки формулювань визначень і теорем? Компіляція автоматично згенерованого коду ставала підтверджуваним сертифікатом. Ось що сталося в довшій серії, яку я зробив з Арістотелем @HarmonicMath. Дякую @PietroMonticone та @llllvvuu за допомогу з налаштуванням креслення. Тут я представляю повну правильну автоформалізацію статті мого друга Стефана Бараньчука про послідовності поділу Чебишева. Код складається приблизно з 5000 рядків дуже нетривіального Lean. Вона виправляє всі невідповідності та прогалини в основній статті (навіть доводить деякі делеговані положення). Я збираюся опублікувати серію таких експериментів, які доведуть, що в деяких галузях математики, включно з елементарною теорією чисел, комбінаторикою та аналізом (усім, що охоплює Mathlib), ми недалеко від масштабного зсуву в документуванні достовірності доказів. Думаю, цей рік буде дуже насиченим!

Якби я був студентом сьогодні, взаємодія з найсучаснішими LLM здавалася б майже списуванням. Сьогодні вранці я випадково сфотографував дошку і попросив ChatGPT-5.2-Pro пояснити контекст, розв'язок і деякі побічні зауваження щодо відомої теореми Чевеллі про конструктивні множини. Те, що я отримав, було надзвичайно глибоким звітом, який синтезував якісний матеріал з алгебраїчної геометрії, взятий з усього інтернету. Це породжує серйозне питання: які справжні зусилля та виклики для студентів сьогодні? Вартість — це, безумовно, один із факторів, але коли доступ до цих моделей з'явився, як можна навчатися в цій країні достатку, де пояснення, посилання та інтерактивне дослідження доступні миттєво? Можливо, боротьба вже не в тому, щоб отримати інформацію чи навіть зрозуміти окремі аргументи, а в розвитку судження: знати, які питання ставити, яким поясненням довіряти, як розпізнавати глибину чи поверхневу правдоподібність, і як внутрішньо засвоювати ідеї, а не просто їх споживати. У середовищі, де відповідей багато, справжня складність може полягати у формуванні смаку, математичної інтуїції та здатності орієнтуватися — а не тонути в цьому раптовому надлишку знань.