Beberapa bulan yang lalu, hasil matematika AI mulai membuat berita. Wajar saya penasaran apakah saya, seorang pemula matematika, dapat menemukan masalah terbuka dan memiliki model frontier mengatasinya. Memakan seluruh satu bulan waktu bebas dan beban token yang besar, tetapi saya percaya saya telah mendapatkan bukti Lean dari konjektur refinement Conway, yang ditajuk 50 tahun yang lalu.

Konjektur menyatakan bahwa jika ab = cd, ada bilangan bulat e, f, g, h sehingga a = ef, b = gh, c = eg, dan d = fh. Buktik saya belum diverifikasi secara independen oleh ahli matematika. Namun, saya memiliki alasan yang baik untuk percaya bahwa benar dan secara sungguh-sungguh mengundang penyangkalan.

Buktik telah melewati pemeriksaan mekanik dari pendaftaran Palomar, dan orang yang familiar dengan Lean dan bidang tersebut mengatakan pernyataan itu terlihat benar. Jadi, dengan asumsi tidak bergantung pada bug kernel, kemungkinan itu adalah yang sah. Dalam postingan ini, saya akan menggambarkan pendekatan saya dan hal yang saya pelajari.

Memilih Bidang Saya meminta Claude memilih masalah terbuka dalam program penelitian bilangan surreal. Bilangan surreal adalah penemuan John Conway, sistem angka yang menyertakan semua angka besar dan kecil: semua bilangan real, bilangan ordinal seperti omega yang sangat besar, dan kombinasi seperti 75 + omega*3 + 1/omega. Yang menakjubkan adalah bahwa sistem yang kaya ini lahir dari satu aturan: menyerangkan angka baru di setiap celah di antara angka yang sudah ada.

Memilih Masalah Semula, saya meminta Claude untuk masalah yang tidak terselesaikan dalam program penelitian bilangan surreal.