Matematika Terformal dengan Lean

Lean adalah bahasa pemrograman yang dipakai untuk memformalkan matematika sehingga teorema, struktur, dan bukti bisa diperlakukan seperti kode dan diverifikasi secara statis.

Bukti dalam Lean ditulis sebagai rangkaian taktik; taktik seperti rfl dan exact menutup goal yang sah, sedangkan sorry menonaktifkan pemeriksaan dan sebaiknya diganti.

Menambahkan aksioma keliru (mis. 2 = 3) memungkinkan pembuktian kontradiktif seperti 2 + 2 = 6, menegaskan pentingnya konsistensi sistem aksioma.

Contoh sederhana menunjukkan cara menggunakan taktik rfl dan rewrite serta efek penghapusan aksioma salah untuk memulihkan konsistensi.

Proyek besar seperti formalisasi Teorema Terakhir Fermat sedang berlangsung; masih banyak sorry yang akan dihapus seiring kemajuan komunitas.

Penulis merekomendasikan sumber pembelajaran Lean seperti Natural Numbers Game, Mathematics in Lean, dan komunitas Zulip.