تعریف کتاب افسانه‌ی پادشاه و ریاضیدان رو بار اول اول محمد طبیعی شنیدم؛
کتاب، نمایشنامه‌ای هست با عمق کمی از ریاضی و شاید نظریه‌ی گراف!
نویسنده‌های کتاب، نغمه ثمینی و مهدی بهزاد هستن و هدفشون از نوشتن کتاب، ترویج ریاضی بوده. کتاب، داستانی تخیلی از پادشاه کم سوادی رو روایت می‌کنه که برای نجات کشورش با موانعی روبرو می‌شود که به کمک معماهای ریاضی حل می‌شن.
حجم کتاب خیلی کمه (۱۵۰ صفحه) که به شکل نمایشنامه نوشته شده.
خلاصه برای استفاده‌ی مفید از آخر هفته، توصیه می‌کنم کتاب رو بخونید :)

#کتاب

اینم اثبات شد!
ظاهرا پنج ساعت طول کشید.
https://www.erdosproblems.com/forum/thread/481

طرف ایمیل زده به استاد، متن ایمیل رو چت جی پی تی براش نوشته، یادش رفته اسمش و... رو بنویسه.

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

طرف ریاضیدانه و به یکی از دوستان یا فامیل هاش گفته آخرین کار من در مورد
inequalities
بوده، دوستش هم گفته که تو خیلی
woke
هستی! (یعنی نسبت به مسائل اجتماعی، عدالت و ... حساس هستی)

نظریه انواع شهودگرایانه

مقدمه

نظریه انواع شهودگرایانه¹، همون طور که از اسمش پیداست، یک سیستم نوع‌دهی² بر اساس منطق شهودی‌ئه. منطق کمونیستی شهودی³ خیلی خلاصه، با برهان خلف مخالفه و کلا می‌گه «باید مثال نقضت رو بسازی تا مخالفتت رو به حساب بیارم و الا برو پی زندگیت😁». به عبارت دیگه، برهان رو ساختاری می‌خواد و سور وجودی رو جدی می‌گیره؛ وقتی شما می‌گید «وجود دارد فلان چیز که...» یه شهودگرا حتما ازتون می‌پرسه «کجا و با چه ماهیتی وجود داره؟» (خودم معتقدم که «به شما چه مربوط، وقتی می‌گم هست یعنی هست. فضول‌های انقلابی😂»)

نوع‌دهی با اغماض زیاد، فرایندی هست شبیه تعریف کردن نوع برای متغیرها در برنامه‌نویسی، مثل
int a = 3

این مورد رو صرفا برای پیدا کردن شهود گفتم و الا داستان یه چیزی فراتر از اینه (نوع‌ها یه جوری وجود «برهان ساختاری» برای یک گزاره رو تضمین می‌کنن) که جلوتر بهش می‌رسیم.

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

پانوشت:
¹ Intuitionistic Type Theory
² Typing
³ Intuitionistic logic

منابع:
• Logic and Structure, D. van Dalen
• Lectures on Curry-Howard Isomorphism, M. H. Sørensen and P. Urzyczyn
• On Brouwer, M. van Atten
• Per-Martin Löf:
- On the Meanings of Logical Constants and the Justifications of the Logical Laws
- Intuitionistic Type Theory

@simplytypedexistence

یه قضیه مهم در آنالیز تابعی
Invariant subspace problem
هست.
منتها این قضیه یه داستان تاریخی داره.
برنشتاین–رابینسون در دهه ۱۹۶۰ در آنالیز غیر استاندارد اون رو اثبات کردند، در همون شماره مجله ای که این قضیه اثبات می شه اثبات هالموس هم از این قضیه ارائه می شه، منتها اثبات با روش های آنالیز کلاسیک بازنویسی می شه.
خیلی ساده بخوایم بگیم در آنالیز غیر استاندارد مفهوم حد رو می ذارند کنار و از اعداد بی نهایت کوچک و بزرگ استفاده می کنند.
بعضی ها می گند این تصمیم شاید تا حدی به خاطر نگاهی بوده که به آنالیز غیر استاندارد وجود داشته(چاپ اثبات آنالیز غیر استاندارد و بعد کلاسیک‌سازی فوری اون، نوعی بی‌اعتمادی یا احتیاط نسبت به NSA رو نشون می‌ده)
عکس هم هالموس هست در جوانی.

#دانستنی های_ به درد_نخور ۴۰
می دونستید که نماد سیگما رو اولین بار فوریه و درسال ۱۸۲۰ به کار برد؟
حرف سیگما به صورت بزرگ، با حدودش که در بالا و پایین نوشته می شه.

از بین اثبات هایی که برای واگرایی سری هارمونیک اومده و تعدادشون هم کم نیست، این یکی از جمع و جورترین ها است. از این خاصیت هم استفاده کرده:
e^x>1 + x
ظاهرا یه ریاضیدان به عنوان حل تمرین اون رو نوشته بوده.

اگر کورت گودل امروز استاد بود:
هر سیستم سازگار و قابل بازنمایی به‌صورت بازگشتی که توانایی بیان حساب ابتدایی را دارد، شامل گزاره‌های تصمیم ناپذیر است.
دانشجو: داداش، این توی امتحان میاد؟

گویند پل اردوش، ریاضی‌‌دان مشهور مجارستانی، یحتمل تحت تأثیر همکارش آلفرد رنیی که معتاد به قهوه بوده و می‌گفته «ریاضی‌دان ماشینی است که قهوه را به قضیه ریاضی تبدیل می‌کند»، عین چی قهوه می‌خورده. بعد از فوت مادرش دیده قهوه جواب نمی‌ده، رفته سراغ ریتالین و آمفتامین. وسط حال کردنش با سوپرمن بودن، رون گراهام (همکار دیگری) از سر رفاقت می‌گه «داش گلم پل، حالا که هر چی می‌گم آمفتامین نزن، گوش نمی‌دی، بیا شرط ببندیم حداقل یک ماه نخوری مغزت نترکه؛ اگر یک ماه دووم آوردی من بهت ۵۰۰ دلار می‌دم (حساب کنید دهه ۷۰ میلادی چه قدر پول بوده). اگر نه که خود خوشگلت باید سر کیسه رو شل کنی».

اردوش هم با ژست «حالا می‌بینی حسابت رو خالی می‌کنم» می‌ره برای برآورده کردن شرط.

و...

می‌بره! اما به قول خودش (خطاب به گراهام)، «یک ماه ریاضیات عقب می‌افته!»:

شرط ما نشون داد که من معتاد نیستم. ولی این یک ماه هیچ کاری نکردم! صبح از خواب پا می‌شدم عین منگ‌ها زل می‌زدم به کاغذ خالی! عین آدمای معمولی هیچ ایده‌ای نداشتم! تو ریاضیات رو یک ماه عقب انداختی!

بعدم برمی‌گرده به ریتالین و آمفتامین.

فقط اگر امروز زنده بود، بهش می‌گفتم اردوش جان، اینی که گفتی دقیقا سندرم ترک محرکه و شرمنده، شوما معتادی:))

پ.ن: اون زمان محرک تا حدی مثل نقل و نبات بوده و حتی بدون نسخه تجویز می‌شده، تا عوارضش اومد رو و باعث شد فقط به بیش‌فعال‌ها اونم با قسم آیه و هزارتا سند بدن:))

این مثل اینکه قبلا حل شده بود، در یک مقاله در سال ۱۹۸۱. به لحاظ حال گیری:
انسان 1 - هوش مصنوعی 0.

در یه کتاب فارسی خونده بودم به نقل از هایزنبرگ گفته بود: تنها ابزار ریاضی که در مکانیک کوانتوم نیاز دارم ماتریسه(جای دیگه پیدا نکردم، مطمئن نیستم در مورد این جمله)

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

البته می دونم که هر کس باید با تلاش و سخت کوشی و تمرین زیاد و مطالعه عمیق و ... به درک از مفاهیم ریاضی برسه، ولی کلیت این ماجرا به نظرم کمی مشکوکه!

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

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

باعث قهقه شاید نشه، ولی ریاضی دوست(دان) پسنده!
شوخی با ندانسته های بزرگ.

فرمال متد با اغماض زیاد، یکی از کاربردهای منطق تو علوم کامپیوتره. منطق ریاضی رو بشین از کتاب فان‌دالن یا دکتر اردشیر بخون ببین خوشت میاد یا نه. نظریه زبان‌ها و ماشین‌ها رو هم خوب یاد بگیر، بعدش فکر کن به بقیه‌ش.

بعد این که دانشگاه معمولی و دسته‌ی بیل. داری چیزی رو که دوست داری می‌خونی و همین برای ادامه کافیه.

من رشته‌م ریاضی نبوده، نمی‌تونم مسیر دقیقی بدم. ولی جبر و lattice theory توی کار من دید خوبی به آدم می‌ده.

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

آقای
Ken Ono
که یه نامبر تئوریست درجه یک هم هست، تصمیم گرفته بعد از سال ها فعالیت در دانشگاه، قید دنیای آکادمیک رو بزنه و بره تو استارتاپی که شاگرد ۲۴ ساله اش راه انداخته کار کنه.
این خانم هم استارتاپش حسابی سروصدا کرده و مساله های معروف اردوش رو حل کرده.
استاد می گه نسبت به هوش مصنوعی نگاه مثبتی نداشته و فکر می کرده هیاهو باشه، بعد دیده قضیه جدیه. گفته اگر بخواد خیلی بروز باشه مجبوره بره سمت هوش مصنوعی. تصمیم گرفته راه جدیدی رو انتخاب کنه، راه متفاوتی برای انجام ریاضی.
این شرکت
لینک مربوط