ظاهرا بهترین مدل های هوش مصنوعی هم در تشخیص اینکه فلان گره چه گره ای هست، دچار اشتباه می شند‌.
برای اینکه همه گره ها رو بتونند بشمارند و دسته بندی کنند یه سری جدول درست کردند، حتی اگر همین جداول استاندارد هم نشون بدی بهشون، نمی تونند درست تشخیص بدند نوع گره رو.
کاری که برای انسان ها هم کم و بیش سخته.

تصویری از یک مقاله فیزیک در سال ۱۹۲۵.
مفهوم ماتریس اون زمان هنوز برای فیزیک دان ها چندان جا نیفتاده بود، برای همین مجبور شدند ضرب دو تا ماتریس رو در مقاله توضیح بدند.
ظاهرا در اون سال ها هنوز جبر خطی به صورت سیستماتیک تدریس نمی شده و خیلی ها مفهوم ماتریس رو درست نمی شناختند.

استنلی آسیموف در پیشگفتار کتاب Yours Isaac Asimov نوشته که آیزاک در طول بیشتر از 50 سال دوران کاریش، حدود 100000 تا نامه دریافت کرده که به 90 درصد اونها پاسخ داده و تخمین می‌زنه که اگر به جای صرف وقتش برای جواب دادن به اون نامه‌ها کتاب می‌نوشت، می‌تونست 100 عنوان کتاب دیگه به کارنامه‌ش اضافه کنه😐

خودش جمله ای داره که می گه:

نوشتن برای من اندیشیدن از طریق انگشتانه.

حدود ۵۰۰ تا کتاب نوشته و نوشتن ۱۰۰ کتاب دیگه با توجه به کارنامه اش خیلی اغراق آمیز نیست، جمله ی دیگه ای داره که می گه:

ممکنه هر کتاب ام رو کسی بتونه بهترش رو بنویسه ولی مجموع آثارم از نظر کیفیت و تنوع غیرقابل تکراره.

شطرنج معمولی دیدند خیلی سخته و از پسش بر نمیاند رفتند سراغ ورژن ها و مدل های دیگه ای از شطرنج.
یه برآورد تقریبی از کل تعداد موقعیت های ممکن در شطرنج که به عدد شانون معروفه حدودا
10¹²⁰
تا است، که همینم با فرضیاتی به دست اومده.

این شطرنج ۵ در ۵ هم به شطرنج گاردنر معروفه و کامل حل شده. مهره های سمت شاه حذف شدند، حرکت
en passant
و قلعه ممنوعه. بررسی کردند و به این نتیجه رسیدند که وضعیت نهایی بازی مساویه(یعنی اگر دو حریف بهترین حرکاتشون رو انجام بدند بازی مساوی می شه)

#دانستنی های_ به درد_نخور ۳۲
می دونستید هاوکینگ یه بار یه مهمونی برای مسافران زمان برگزار کرد؟ این شکلی بود که اول مهمونی رو برگزار کرد(همه چیز رو آماده کرده بود شامپاین، تزئینات، بادکنک و...) بعد دعوت نامه ها رو منتشر کرد. می گفت: اگر مسافری از آینده باشه، میاد و در مهمونی شرکت می کنه!

وضعیت جستجو برای کلمه
quadratic formula
که مربوط به فرمول معادله درجه دوم می شه.
ظاهرا الگوی ثابت و تکرار شونده ای داره:
در بهار جستجو زیاد می شه، در تابستان کم، در پاییز زیاد و در زمستان کم.

این سودوکو رو می گند سخت ترین سودوکوی طراحی شده است.
یه ریاضیدان فنلاندی اون رو طراحی کرده، تعداد خونه های پرشده اش کمتر از جدول های دیگه است.
اگر از حدس استفاده کنید کمکتون نمی کنه، حتی ممکنه گمراه کننده باشه، چیزی که در نهایت کمک کننده است منطق خالص هست.

ریچارد فاینمن دوبار ازدواج کرد.
در سال ۱۹۵۶ از همسر دومش جدا شد.در دادخواست دلیل طلاق
extreme cruelty
عنوان شده.

برای یه set theorist آلمانی که الان در ژاپن ساکن هست.

امروز تولد
Mary Watson Whitney
هست. پدرش در زمینه املاک کار می کرد و تونست شرایط مالی خوبی براش فراهم کنه. در دانشگاه با یه اخترشناس معروف آشنا شد، در اون زمان زنان نمی تونستند دانشجوی رسمی بشند و به عنوان مهمان در کلاس ها شرکت می کرد. برای رفت و آمد از در ورودی دانشگاه تا کلاس ها یه همراه داشت تا مقررات دانشگاه درباره حضور زنان رعایت بشه! زمینه کاری اش ریاضیات، نجوم و مکانیک سماوی بود.
جمله معروفی داره که می گه:

امیدوارم وقتی به بهشت می‌رسم، زن‌ها در اونجا ویولون دوم نزنند!

منظورش اینه که نقش فرعی نداشته باشند.

معروفه که می گند به نش گفته بودند: اگر خیلی فوق العاده ای چرا مساله
embedding problem for manifolds
رو حل نمی کنی؟
و نش اون رو حل کرد.

شاید بشه گفت نش بابت کارهاش در نظریه بازی ها احترام خیلی زیادی از ریاضیدان های محض دریافت نکرد. از جان میلنور نقل شده که استفاده از یه سری قضیه برای اثبات تعادل نش، استفاده نه چندان هیجان انگیز از یه سری قضیه شناخته شده تلقی می شه!
به خاطر کارهاش در نظریه بازی نوبل اقتصاد گرفت، در ریاضیات هم در زمینه توپولوژی، pde ها و... کار کرد که جایزه آبل رو به خاطر کارهاش برنده شد.

Lean 4 with a Math Textbook - Part 3 - Properties of Subsets — Some opinions, held with varying degrees of certainty.
https://filip.lajszczak.dev/lean-4-with-a-math-textbook---part-3---properties-of-subsets.html

وقتی تو یه جمعی می گی من پایان نامه ام رو با ورد نوشتم و از لاتک بهتره.

یه مقاله توی arXiv گذاشتند و ادعا کردند که
Hodge conjecture
رو حل کردند. این حدس یکی از اون حدس هایی هست که جایزه یه میلیون دلاری براش تعیین کردند(در کنار فرضیه ریمان و P vs NP)
ظاهرا متوجه شدند که از این مقالاتی هست که با کمک هوش مصنوعی نوشته شده و در کل چرت و پرته.
واقعا به رسوایی و بی آبرویی اش نمی ارزه. چطور ریسک می کنند و همچین کاری می کنند؟ خب می رفتی سراغ یه مساله ساده تر و کمتر معروف. به هر حال ظاهرا به ۲۴ ساعت نرسیده دستش رو شده.

یه قضیه ظاهرا توی نظریه گره هست به اسم
Alexander's theorem
حالا خانم Nancy Scherich که استاد دانشگاه است و به ترکیب ریاضی و رقص و این چیزا علاقه داره سعی کرده نه تنها صورت قضیه بلکه اثباتی از اون رو هم در یک فیلم کوتاه به کمک رقصنده ها بیان کنه.
https://gallery.bridgesmathart.org/exhibitions/2024-bridges-conference-short-film-festival/nancy-scherich

دیگه حتما می دونید که در ریاضیات مدرن
formal proof
خیلی اهمیت پیدا کرده.

حالا چی هست؟ چرا فرمال؟
چون زبان انسان پر از میان بر و شهود هست. کمی ابهام داره(حالا هر چقدر دقیق باشه اثبات) یه جاهایی می نویسند واضحه که، یا نتیجه می گیریم که. حالا در formal proof که به کمک کامپیوتر انجام می شه این بازی ها وجود نداره، همه چیز دقیق هست. هر تعریف، هر قضیه. پرشی وجود نداره.

چی کار می کنند؟
از proof assistant ها استفاده می کنند، مثل Lean یا Coq. اینا دستیار اثبات هستند. به کمک این ها اون اثبات ها رو انجام می دند.

حالا چی شده بود؟
ژانویه ۲۰۲۴ تائو و یه ریاضیدان دیگه گفتند کی می تونه
strong Prime Number Theorem
رو بیاد یه اثبات رسمی براش بنویسه. کجا؟ توی
Lean
کلی دانشجو و برنامه نویس و... با هم در این کار مشارکت کردن، ولی پروژه به سرانجام نرسید(یه بخشی رو پیش بردند و کار کامل نشده) آدم هایی که همدیگر رو اصلا ندیدند و شاید هیچ وقت نبینند.

الان چی شده؟
می گند Gauss تو سه هفته کار رو جمع کرده(اون گاوس نه، این اسم یه
autoformalization agent
هست.)

۲۵۰۰۰ خط کد با حدود ۱۰۰۰ تا تعریف و قضیه.
https://www.math.inc/gauss
https://github.com/math-inc/strongpnt

حواسم به این نکته نبود که خود گاوس روی اون قضیه کار کرده بود و حالا نرم افزاری به همون اسم یه اثبات فرمال ارائه داده براش(ظاهرا گاوس اولین بار ۱۶، ۱۷ سالگی درگیر این قضیه می شه)
یه نکته دیگه اینکه ظاهرا تائو و... در اون بخش از اثبات که به تابع زتا ریمان مربوط می شده به چالش خوردند.
و نکته آخر: Gauss هنوز به کمک انسان نیاز داره و کل کار رو خودش انجام نداده.