Тут я знову представляю повну автоматичну формалізацію нещодавньої роботи з математики! Баранчук, Стефан. "Зменшення кількості рівнянь, що визначають підмножину 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