این رو
Aristotle
اثبات کرده، یه
IMO-Level Theorem Prover
حل مساله خیلی مقدماتی در اومده و می گند در نهایت در حد مسائل مسابقات ریاضی هست. اینقدر ساده بوده که شک کردند به اثبات. برای همین توی
Lean
هم اثبات شده.
طبق معمول دو نگاه وجود داره:
یه سری می گند کار خاصی نکرده یه مساله در حد مسابقات ریاضی حل کرده.
ضمنا فعلا ورژن کمی ساده تر مساله حل شده. می گند اینکه سی سال هست حل نشده شاید به خاطر اینه که کسی جدی سراغش نرفته.

اون طرف هم مثل همیشه کسانی رو سر ذوق آورده که کی بشه دپارتمان های ریاضی رو تعطیل کنیم!

یه عده می گند مساله بازی رو بعد از سی سال حل کرد، یه عده هم می گند اگه مساله حل کن هست چرا فرضیه ریمان رو حل نمی کنه؟
بحث کامل در همون لینک بالا اومده.
پ ن: اگر راه حل مقدماتی داشته چطور به ذهن غول هایی مثل اردوش، گراهام و...نرسیده؟

یه سوال زیبای دیگه با راه حل

دیروز تولد
Richard Borcherds
بود. فیلدز مدالیست. در زمینه
Quantum field theory
هم کار می کنه.
کانال یوتیوب هم داره، در زمینه بیشتر مباحث دانشگاهی عموما جبری لکچر گذاشته. خیلی ساده دوربین رو می ذاره بالای سرش، رو کاغذ می نویسه و بعد می ره سراغ بحث بعد و کاغذ بعدی.
https://youtube.com/@richarde.borcherds7998?si=HgJnzITDEYdKcaDA

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

دیروز تولد ChatGPT هم بوده. سه ساله شد.
همکار یا شاید هم رقیب ریاضیدان ها.
ترکیب خلاقیت انسانی با توانایی مدل در ایده پردازی تا اینجا بد نبوده.
در هر صورت به نظر میاد مسئولیت نهایی درستی یا نادرستی اثبات با خود انسان باشه.
باید دید ادامه کار چه طوری پیش می ره.

یه گروه مهم در ریاضی، فیزیک، رباتیک، کامپیوتر و مکانیک کوانتومی
SO(3)
هست. چیه اصلا؟
ماتریس های سه در سه مثل A که
A^t*A=I , det(A)=1
منظور از A^t ترانهاده A هست.
این گروه طول و فاصله رو حفظ می کنه. می چرخه ولی فضا رو وارونه نمی کنه!
این گروه
simply connected
نیست. اثبات فنی اش در کتاب ها هست. اثبات غیر فنی و شهودی اش اینجوریه:
فرض کنید یه بشقاب سوپ دارید و نمی خواید بریزه، پس همیشه افقی نگه می دارید اون رو. بشقاب رو ۳۶۰ درجه می چرخونید، بشقاب سر جای اولش هست ولی دست شما به طور کامل پیچ خورده! این یعنی مسیر بسته است(شروع و پایان یکسانی داره)
ولی نمی شه این مسیر رو به یه مسیر ساده که هیچ پیچش بازویی نداره کوچیکش کرد، یعنی یه حلقه ای داره که قابل جمع شدن نیست.
گروه
SO(3)
چرا مهمه؟
چون همه حرکات چرخشی در دنیای واقعی ما عضو این گروه هست.

محاسبه اون انتگرال معروف با یه روش دیگه و استفاده از خواص تابع گاما

نیوتن و رازورزی

فایل ارائه و مقاله‌ی استخراج شده از ارائه‌ی بالا

آیزاک نیوتن معمولاً نماد عقلانیت و نقطهٔ آغاز علم مدرن دانسته می‌شود، اما بخش بزرگی از فعالیت‌های او در کیمیاگری، الاهیات و تفسیر کتاب مقدس بوده است. این مقاله نشان می‌دهد که این دو چهرهٔ به‌ظاهر متعارض ــ نیوتنِ فیزیک‌دان و نیوتنِ کیمیاگر و الاهی‌دان ــ در چارچوبی عمیق‌تر قابل فهم‌اند؛ چارچوبی که در آن «رازورزی» نقش تعیین‌کننده دارد. ابتدا زمینهٔ تاریخی و فکری قرن هفدهم و تأثیر سنت دکارتی، گالیله، کپلر و بویل بر اندیشهٔ نیوتن بررسی می‌شود و سپس وحدت‌بخشی او در نظریهٔ گرانش، همراه با مفاهیمی چون فضای مطلق، زمان مطلق و کنش از دور تحلیل می‌گردد. در ادامه نشان داده می‌شود که عناصر کیمیاگری و الهیاتی نه حاشیه‌هایی شخصی، بلکه منابعی برای شکل‌گیری مفاهیم بنیادین نیوتنی بوده‌اند. سرانجام، پیامدهای این سبک اندیشه برای پژوهش و آموزش علم امروز تبیین می‌شود و استدلال می‌گردد که ویژگی «رازورزی» نیوتن نیرویی محرک برای خلاقیت نظری و پرسش‌گری بنیادی بوده است.

فایل مقاله

فایل ارائه

فایل صوت ارائه

آن‌ها ضرباتشان را دوچندان دوچندان بر دشمن فرود آوردند.

ظاهرا شکسپیر نویسنده ای نبوده که فقط با کلمات سروکار داشته باشه، با اعداد هم آشنایی داشته.
دوران شکسپیر دورانی بوده که ریاضیات هم داشته خودی نشون می داده.
هفت روز، صد هزار سرباز، چهل سال و... تعابیری هستند که در کتاب هاش وجود داره. منتها کمی شاعرانه اعداد رو به کار می برده. یه جا گفته:
thrice-double ass
یعنی ۶ خر!
به جای two از کلمه قدیمی
twain
استفاده کرده.
کلمه
score
رو به معنی بیست به کار برده، مثلا
three score and ten
یعنی ۷۰.
Six score
یعنی ۱۲۰.
https://www.folger.edu/blogs/shakespeare-and-beyond/shakespearean-numbers/

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

#کتاب

اینم اثبات شد!
ظاهرا پنج ساعت طول کشید.
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
ظاهرا یه ریاضیدان به عنوان حل تمرین اون رو نوشته بوده.

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