عیب می جمله بگفتی، هنرش نیز بگو
به gpt-5-pro یه open problem در زمینه
convex optimization
دادند مساله رو حل کرده. بررسی های اولیه نشون می ده اثباتی که ارائه کرده درست بوده.
اومده کران مساله رو کمی بهبود داده.

البته بعضی ها می گند اثباتی ارائه نکرده یه خروجی تولید کرده که بعدا با بررسی معلوم شده درسته!(خودم نفهمیدم این بخش رو)

یکی هم گفته: بپرس ازش
9.11 > 9.9?

با لپ‌تاپ این لینک رو باز کنید، چهار خط پایین‌تر، جایی که تعریف قضیه با نقطه تموم شده، بزنید روی proof تا برهانش باز شه. ایشالا که نمی‌گرخید 😁
این عکس هم از بخش دیگری از همین کدبیس هست.
هم‌چنان disclaimer که کد مال من نیست.
این که چی رو داره اثبات می‌کنه، از حوصله بحث خارجه. صرفا گذاشتمش که ببینید برهان کامپیوتری چه قدر می‌تونه پیچیده باشه. برای همین یه دونه اثبات فقط 6 تا تاکتیک لوکال مستقیم نوشته. Implicitهاش و وارداتی‌هاش از فایل‌های دیگر بماند:))

چرا قضیه های ریاضی رو قبول می کنیم؟ چون اثبات داریم براشون. خود اون قضیه ها براساس یه سری تعریف و axiom بدست اومده، چرا اون اصل ها رو قبول می کنیم؟ چون بدیهیه!
مقاله معروف Believing the Axioms نوشته آقای خانم
Penelope Maddy
یکی از بهترین مقالات در زمینه فلسفه ریاضی و اصول نظریه مجموعه ها است. قبلا فکر می کردند(به ما هم کم و بیش اینجوری گفتند) چون اصول بدیهی هستند اون ها رو می پذیریم، ولی Maddy می گه اینا خیلی هاشون بدیهی هم نیستند، اون ها رو می پذیریم چون نظریه رو غنی می کنند، یعنی پیامدهای سودمندی دارند.
حال داشتین بخونید.
بعدا بخش هایی از اون رو می ذارم.
https://jwood.faculty.unlv.edu/unlv/Articles/Maddy1.pdf

معروف ترین مساله باز در ریاضی رو گام به گام توضیح داده
The Riemann Hypothesis, explained | by Jørgen Veisdal | Cantor’s Paradise
https://www.privatdozent.co/p/the-riemann-hypothesis-explained-478?utm_source=publication-search

نامه
Richard Feynman
به همسرش، بعد از مرگش
ازدواجشون هم ماجرایی داشته، قبل از ازدواج همسرش مبتلا به سل بوده که در اون زمان غیرقابل درمان بوده و می دونستند که زیاد زنده نمی مونه، به رغم مخالفت شدید خانواده فاینمن این ازدواج شکل می گیره و باقی ماجرا...

البته در مورد تصویر سمت راست، توپولوژی استثنا است.
یه کتاب در این زمینه.

شاید حق با آقای Ribet بوده!
یه تمرین از همون کتاب...

چند نکته در مورد معادلات درجه سوم:
اولین دسته بندی درست و درمون و تلاش برای حل رو خیام انجام داد. ۱۴ حالت مختلف برای معادله در نظر گرفت و اون ها رو حل کرد.
این مساله تو تاریخ جبر خیلی مهمه چون اولین نگاه سیستماتیک به حل معادله درجه سه بوده.

توی ایتالیا یه زمانی رسم بود که به ریاضیدان ها می خواستند پست بدند (چون رقابت زیاد بود) مسابقه برگزار می کردند. سوالات مسابقه هم معمولا معادلات درجه سه و چهار بود.

خود تلاش برای حل این معادله باعث شد ریاضیدان هایی مثل گاوس اعداد مختلط رو جدی بگیرند.

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

انیشتین اینجا رابطه
E=mc²
رو توضیح می ده.
نکته جالب توجه accent اش هست.

ماموریت فضایی در اون سال ها بدون ریاضیات(به ویژه حل عددی معادلات دیفرانسیل) غیر ممکن بود. در اون سال ها شوروی به لحاظ سخت افزاری از آمریکا عقب بود و به محاسبات عددی کارآمد وابسته بود.
مساله این نبود که ریاضیدان ها و مهندس ها توانایی محاسبه نداشتند، احتمالا به خاطر فشار حزب هشدارهای علمی رو نادیده گرفتند.
ریاضیات کار خودش رو کرده بود، ولی سیاست اون رو کنار گذاشت.

FLT is not applicable to matrices

دوستان می گند این real math نیست. اون چیزی که
Alexander Grothendieck
معرفی کرده ریاضی هست.
The Langlands Program
ریاضی واقعیه.
نظر خاصی ندارم خودم.

کتاب جدید یکی از شارلاتان ترین فیلسوف های معاصر هم قراره به زودی منتشر بشه. این دفعه استاد رفته سراغ مکانیک کوانتوم!
البته ظاهرا طبق معمول و مثل همیشه سراغ لاکان هم رفته.
در کتاب سوکال حسابی به لاکان پرداخته شده‌.

یه ماجرایی هم معروفه در موردش که می گند بدون دیدن فیلم آواتار و فقط براساس شنیده هاش یه نقد مفصل بر اون می نویسه.

آقا من این‌جا اشتباه کردم (و یه کم دیر هم بهش پرداختم): جمله رو طوری نوشتم که انگار در Coq چیزی به نام Implicit Tactic داریم. واژه implicit تا این‌جا که می‌دونم، بخشی از دستورهای مربوط به Arguments هست، مثلا:

Set Implicit Arguments

که می‌گه Coq (در صورت امکان) تایپ آرگومان‌ها رو خودش دربیاره و ما لازم نباشه دائم دستی ورودی بدیم.

اینجا یه کم informal به کار بردمش، به این عنوان که «طی اون برهان الگوهایی می‌تونه وجود داشته باشه که خودشون بشن یه تاکتیک جدا».

و الا به قاعده، چنین مفهومی رو در Coq نداریم.

خلاصه عذر می‌‌خوام:")

یه سری می گند که درگیرشدن با بی نهایت منجر به دیوانگی کانتور شد، که البته نظر درستی نیست.
ظاهرا از اختلال روانی رنج می برده که شاید
schizoaffective
بوده یا چیزی نزدیک اون یا اختلال دوقطبی.
درگیر مشکلات خانوادگی و مالی هم بوده. با نظریه مجموعه ها هم اون اوایل خیلی مخالفت شد. درگیر کارهای فلسفی و الهیاتی هم شده بود(از جمله یکی کردن set theory با الهیات مسیحی)
ولی احتمالا دلیل اصلی بیماری اش زمینه ژنتیکی داشته.

https://news.1rj.ru/str/IMHStudents/752
در رابطه با اینکه کارکرد توپولوژی جبری چیه صحبت کردیم.

کتاب های کتابخونه شخصی Ulam
البته اینجا فقط کتاب هایی که مربوط به شطرنج هست رو می بینید.

1961

طرف در مورد قاعده ساروس مقاله نوشته، cite خورده!