ගත සතියකදී AI පද්ධති ගණිත ලෝකයේ නව මට්ටමකට පියනැගුණා. ChatGPT, Logical Intelligence සහ OpenAI හි නවතම මොඩලය Sol, එකට එක්ව Erdősගේ Unit Distance අනුමානය සඳහා විරුද්ධ උදාහරණයක් සොයාගැනීමෙන් පසුව, ඒක Lean නමැති ආධාරක පද්ධතියේ සත්ය ආකෘතියක් බවට පත් කරලා.
මූලිකව, ChatGPT විසින් 1960 දශකයේ Golod‑Shafarevich නාමික සූත්රය භාවිතා කර, ඒ අනුමානය වැරදි බව පෙන්වූ පර්යේෂණයක් ඉදිරිපත් කළා. එය මිනිස් ගණිතඥයන්ට පෙරදැරි පරීක්ෂණයක් ලෙස සලකුණු කරන ලදි. ඒ පසු, Logical Intelligence හි Field Medalist Mike Freedman එම ලේඛනය සම්පූර්ණයෙන් Lean වෙත ස්වයං-ආකෘතිය කිරීමේ හැකියාවක් තිබේ කියා දැනුම් දුන්නා. මටත්, මගේ post‑doc Thomas Browning ටත් ඒ කේතය පරීක්ෂා කිරීමට අවස්ථාව ලැබුණා.
ඉන් පසු, OpenAI හි Boris Alexeev, Sol නමැති නවතම LLM එක භාවිතා කර, කිසිදු අනුමාන නැතිව, Erdős විරුද්ධ උදාහරණය සම්පූර්ණයෙන් Lean තුළ ආකෘතිකරණය කළා. Sol තුළින් තිදෙනා සති තුනකදී 1.2 මිලියන පේළි Lean කේතයක් නිපදවා, ගෝලීය පන්තිය ක්ෂේත්ර सिद्धान्तයේ (global class field theory) අතිකාලීන තත්වයන් ද සනාථ කළා. මෙය mathlib නාමික පුස්තකාලය (2.3 මිලියන පේළි) වසර අටකට පමණ කාලයක් ගත වූ අංශයක් වඩා වැඩි ප්රමාණයක් වේ.
ශ්රී ලංකාවට ඇති වැදගත්කම
මෙවැනි AI‑ආධාරිත ගණිත ආකෘතිකරණය ශ්රී ලංකාවේ විද්යාල, විශ්වවිද්යාල සහ තාක්ෂණික ආයතන සඳහා විශාල අවස්ථාවක් සපයයි.
- ශිෂ්යයන් – අතිකාලීන ගණිත සංකල්පයන් කුමන පරිදි Lean මගින් සත්ය කරගත හැකිද යන්න පළමු පියවරෙන්ම දැකගත හැකිය.
- ඩිවෙලපර්ලා – AI මොඩලයන් සම්බන්ධයෙන් formal verification ක්රමවේදයන් ඉගෙන ගැනීම, software security සහ blockchain වැනි ක්ෂේත්ර වලට ප්රයෝජනවත්.
- ව්යාපාර – AI‑generated code එකේ නිශ්චිතතාව තහවුරු කිරීමෙන්, R&D වියදම අඩු කර, නව නිෂ්පාදන ඉක්මනින් වෙළඳපලට ගෙන යා හැක.
ඉදිරියේදී, Lean සහ AI එකට අනුබද්ධ වූ පර්යේෂණ වැඩසටහන්, ශ්රී ලංකාවේ තාක්ෂණික මනාපය වර්ධනය කර, ගෝලීය ගණිත සමාජයට දායකත්වයක් ලබා දීමට ඉඩ සලසයි.
අවසන් වශයෙන්, AI‑මගින් නිර්මාණය කළ ගණිත සාධන, මනුෂ්ය විශ්වාසය අභියෝග කරමින්, නව තාක්ෂණික යුගයක් ඇරඹුන බව අපි දැකගන්නෙමු. මේ අත්දැකීම, ගණිතය, පරිගණක විද්යාව සහ AI අතර සම්බන්ධතාවය ගැඹුරු කරමින්, අපගේ අනාගතය තීරණය කරයි.
