Makalah matematika membutuhkan validasi formal. Ini biasanya dilakukan secara informal oleh wasit. Tetapi bagaimana jika kita dapat mengandalkan sesuatu yang lebih kuat seperti formalisasi otomatis menjadi Lean 4 di mana peran wasit akan direduksi menjadi pemeriksaan yang cermat terhadap formulasi definisi dan teorema? Kompilasi kode yang dihasilkan secara otomatis akan menjadi sertifikat bukti. Inilah yang terjadi dalam jangka panjang yang saya lakukan dengan Aristoteles pada tahun @HarmonicMath. Terima kasih kepada @PietroMonticone dan @llllvvuu karena telah membantu pengaturan cetak biru. Di sini saya menyajikan formalisasi otomatis yang benar dari makalah teman saya Stefan Barańczuk tentang urutan perpecahan Chebyshev. Kodenya adalah sekitar 5000 baris Lean yang sangat tidak sepele. Ini mengoreksi semua inkonsistensi dan celah dalam makalah utama (bahkan membuktikan beberapa proposisi yang didelegasikan). Saya akan memposting serangkaian eksperimen semacam itu, membuktikan bahwa dalam beberapa bidang matematika, termasuk teori bilangan dasar, kombinatorika dan analisis (segala macam hal yang dicakup oleh Mathlib) kita tidak jauh dari pergeseran besar-besaran dalam dokumentasi validitas pembuktian. Saya pikir ini akan menjadi tahun yang sibuk!