Mathematical Musings
Photo
ظاهرا اتفاقی افتاده که می گن که گویی بمبی بوده که منفجر شده و همزمان چند تا حوزه رو تحت تاثیر قرار داده یا خواهد داد. ریاضیات، محاسبات کوانتومی، رمزنگاری، دنیای بیت کوین و اتریوم و همین طور بلاک چین رو و حتی جنبه های سیاسی هم داشته.
یه الگوریتمی هست که بهش می گن
Shor's algorithm
برای تجزیه اعداد به عوامل اول به کار می ره. توی رمزنگاری و...به کار میاد.
حالا چی شده؟
تیم
Google Quantum AI
یه مقاله داده بیرون و این الگوریتم رو ۱۰ برابر بهتر کرده.
دیگه اگه کمی با الگوریتم سروکله زده باشین حتما می دونید که یه گام به جلو نیست، یه پرش بلند حساب می شه.
دیگه چی شده؟
گفتند که دولت آمریکا ازشون خواسته detail فنی مقاله رو منتشر نکنند. اینا گفتند روند کار این طوری نیست. باید طی یه مقاله شفاف جزییات کار رو شرح بدیم. ۵۰۰ ساله اینطوریه. بعد دیدند راهی نیست اومدند با روش
zero-knowledge proof
مقاله رو منتشر کردند(به زبان ساده: قانع ات می کنم، ولی جزییات رو نمی گم)
می گن شاید اولین نمونه سانسور دانشگاهی در تاریخ اون هم در این ابعاد.
دور و بر این مساله اتفاقات دیگه ای هم افتاده و اینکه ظاهرا کسانی به نتایج جانبی دیگه ای هم در این رابطه دست پیدا کردند. افراد آماتور و بدون تحصیلات دانشگاهی(یه نوجوان). می گن دوره AI هست و پژوهش داره وارد فضای جدیدی می شه.
یه نتیجه دیگه هم داره این تحقیق و اون اینه که می گن رمزنگاری های فعلی تا حد زیادی امنیتش کاهش پیدا می کنه(شاید حوالی ۲۰۳۵)
https://quantumai.google/static/site-assets/downloads/cryptocurrency-whitepaper.pdf
یه الگوریتمی هست که بهش می گن
Shor's algorithm
برای تجزیه اعداد به عوامل اول به کار می ره. توی رمزنگاری و...به کار میاد.
حالا چی شده؟
تیم
Google Quantum AI
یه مقاله داده بیرون و این الگوریتم رو ۱۰ برابر بهتر کرده.
دیگه اگه کمی با الگوریتم سروکله زده باشین حتما می دونید که یه گام به جلو نیست، یه پرش بلند حساب می شه.
دیگه چی شده؟
گفتند که دولت آمریکا ازشون خواسته detail فنی مقاله رو منتشر نکنند. اینا گفتند روند کار این طوری نیست. باید طی یه مقاله شفاف جزییات کار رو شرح بدیم. ۵۰۰ ساله اینطوریه. بعد دیدند راهی نیست اومدند با روش
zero-knowledge proof
مقاله رو منتشر کردند(به زبان ساده: قانع ات می کنم، ولی جزییات رو نمی گم)
می گن شاید اولین نمونه سانسور دانشگاهی در تاریخ اون هم در این ابعاد.
دور و بر این مساله اتفاقات دیگه ای هم افتاده و اینکه ظاهرا کسانی به نتایج جانبی دیگه ای هم در این رابطه دست پیدا کردند. افراد آماتور و بدون تحصیلات دانشگاهی(یه نوجوان). می گن دوره AI هست و پژوهش داره وارد فضای جدیدی می شه.
یه نتیجه دیگه هم داره این تحقیق و اون اینه که می گن رمزنگاری های فعلی تا حد زیادی امنیتش کاهش پیدا می کنه(شاید حوالی ۲۰۳۵)
https://quantumai.google/static/site-assets/downloads/cryptocurrency-whitepaper.pdf
❤22👍2👎2
Mathematical Musings
Photo
میگه دانشجوی نگونبخت وارد دانشگاه که میشه تازه با سیل اتهامات و انواع قضاوت روبرو میشه. شاید از یه شهر کوچیک یا روستایی اومده به اون دانشگاه و حالا شاید مثلا در ریاضیات ضعیف باشه. ولی دانشگاه فقط براساس یه نمره اون رو قضاوت میکنه و میگه ناآماده است یا ضعیف هست.
توی دبیرستان معلم خوب نداشته، کتابهای درست و درمون نداشته، سرفصلها رو بهش درست نگفتند. بعد کلی بهش پیشنیاز و جبرانی هم میخوره و وقت و هزینهاش به فنا میره.
میگه دانشگاهها کی میخوان فرق این دو تا چیز رو بفهمند؟
opportunity gaps
و
ability gaps
اون نمره ربطی به توانایی اون فرد نداره، فقط فرصت کمتری داشته، شانس برخورداریاش کمتر بوده، شرایط بدتری داشته، همین.
میگه اینکه میگی دانشجو ناآماده است داری چرت وپرت میگی، اون فقط از یه سیستم ناعادلانه عبور کرده.
اگر دانشجو fail میشه، اون شکست نخورده سیستم دانشگاهیه که شکست خورده.
میگه دروس جبرانی رو رها کنید، مستقیم طرف رو بفرستید سر درس اصلی و همون جا همون چیزهایی که ضعف داره رو با
Just-in-Time Support
پوشش بدید.
چند تا دانشگاه این کار رو کردند و نتیجه گرفتند.
https://www.the74million.org/article/why-students-reach-college-underprepared-for-math-and-what-to-do-about-it/
توی دبیرستان معلم خوب نداشته، کتابهای درست و درمون نداشته، سرفصلها رو بهش درست نگفتند. بعد کلی بهش پیشنیاز و جبرانی هم میخوره و وقت و هزینهاش به فنا میره.
میگه دانشگاهها کی میخوان فرق این دو تا چیز رو بفهمند؟
opportunity gaps
و
ability gaps
اون نمره ربطی به توانایی اون فرد نداره، فقط فرصت کمتری داشته، شانس برخورداریاش کمتر بوده، شرایط بدتری داشته، همین.
میگه اینکه میگی دانشجو ناآماده است داری چرت وپرت میگی، اون فقط از یه سیستم ناعادلانه عبور کرده.
اگر دانشجو fail میشه، اون شکست نخورده سیستم دانشگاهیه که شکست خورده.
میگه دروس جبرانی رو رها کنید، مستقیم طرف رو بفرستید سر درس اصلی و همون جا همون چیزهایی که ضعف داره رو با
Just-in-Time Support
پوشش بدید.
چند تا دانشگاه این کار رو کردند و نتیجه گرفتند.
https://www.the74million.org/article/why-students-reach-college-underprepared-for-math-and-what-to-do-about-it/
👍48❤14👎3🤔3🔥2
Mathematical Musings
Photo
چند تا حدس و پیشبینی درباره آینده ریاضیات و AI
میگن حالا اونطوریها هم نیست که ریاضیدانها شلوغش کردند. بخشی از این نگرانی شاید بیشتر صنفی باشه! موقعیت خودشون رو شاید در خطر دیدند و نگران شدند. AI که بیاد اون ساختار موجود رو به هم میزنه. گرنتها شاید حذف بشه، "به من پول بده دارم تحقیق میکنم" دیگه شاید بیمعنی بشه(دست کم در حوزههایی از ریاضیات)، AI شاید کمک کنه که افرادی از بیرون دانشگاه هم بتونند در جریان تحقیقات ریاضی شرکت کنند(این اتفاق الان هم افتاده). این به روند دموکراتیزه شدن علم هم کمک میکنه. این ساختاری که تعریف شده "بیرون" و "درون" آکادمی شاید از اول درست و یا بهینه نبوده. ریاضیدانها در این سالها باور کردند که خودشون و از درون دانشگاه همه کارند و دارند علم رو پیش میبرند. این حرف توی این قرن درست بوده ولی قبلا اینطور نبوده و شاید بعد از این هم اینطور نشه.
به هر حال همه این حرفها پیشبینی هست و مخصوصا در این حوزه(حالا دیگه میشه گفت tech) باید با احتیاط اظهارنظر کرد.
سالها پیش، قبل از اینکه PCهای خونگی متداول بشه، یکی از این "صاحبنظران" گفته بود: اصلا چه دلیلی داره یه فرد توی خونه خودش کامپیوتر داشته باشه؟
تا الان هم بیشتر نظرات درست نبوده. جز شاید بچه زرنگی مثل چامسکی که اینقدر کلیگویی کرده بود که حرفش بعد از چند سال هنوز کم و بیش معتبره و یا آدم باهوشی مثل گاورز که بازه رو اینقدر بزرگ گرفته که هیچکس تا اون موقع زنده نیست که ببینه چی شده؟
هرچند میگن در بعضی حوزهها هر چقدر هم استفاده از AIها فراگیر بشه، یه فرد بیرون آکادمی هر چقدر هم تلاش کنه و دست به دامن هر نوع از هوش مصنوعی بشه امکان پیشبرد علم رو نداره. دست کم فعلا، مثل
Langlands program
میگن حالا اونطوریها هم نیست که ریاضیدانها شلوغش کردند. بخشی از این نگرانی شاید بیشتر صنفی باشه! موقعیت خودشون رو شاید در خطر دیدند و نگران شدند. AI که بیاد اون ساختار موجود رو به هم میزنه. گرنتها شاید حذف بشه، "به من پول بده دارم تحقیق میکنم" دیگه شاید بیمعنی بشه(دست کم در حوزههایی از ریاضیات)، AI شاید کمک کنه که افرادی از بیرون دانشگاه هم بتونند در جریان تحقیقات ریاضی شرکت کنند(این اتفاق الان هم افتاده). این به روند دموکراتیزه شدن علم هم کمک میکنه. این ساختاری که تعریف شده "بیرون" و "درون" آکادمی شاید از اول درست و یا بهینه نبوده. ریاضیدانها در این سالها باور کردند که خودشون و از درون دانشگاه همه کارند و دارند علم رو پیش میبرند. این حرف توی این قرن درست بوده ولی قبلا اینطور نبوده و شاید بعد از این هم اینطور نشه.
به هر حال همه این حرفها پیشبینی هست و مخصوصا در این حوزه(حالا دیگه میشه گفت tech) باید با احتیاط اظهارنظر کرد.
سالها پیش، قبل از اینکه PCهای خونگی متداول بشه، یکی از این "صاحبنظران" گفته بود: اصلا چه دلیلی داره یه فرد توی خونه خودش کامپیوتر داشته باشه؟
تا الان هم بیشتر نظرات درست نبوده. جز شاید بچه زرنگی مثل چامسکی که اینقدر کلیگویی کرده بود که حرفش بعد از چند سال هنوز کم و بیش معتبره و یا آدم باهوشی مثل گاورز که بازه رو اینقدر بزرگ گرفته که هیچکس تا اون موقع زنده نیست که ببینه چی شده؟
هرچند میگن در بعضی حوزهها هر چقدر هم استفاده از AIها فراگیر بشه، یه فرد بیرون آکادمی هر چقدر هم تلاش کنه و دست به دامن هر نوع از هوش مصنوعی بشه امکان پیشبرد علم رو نداره. دست کم فعلا، مثل
Langlands program
👍15👎1
اینجا برای جواب دادن به یه سوال از
mathoverflow
تائو از
ChatGPT
کمک میگیره. میگه تا الان که باهاش کار کردم به hallucination و این چیزا برنخوردم(دست کم تا اون موقع)
میگه استراتژی کلیام اینه که هر چیزی رو گام به گام براش توضیح میدم و بعد از چک کردن جواب میرم مرحله بعد. این سوال و جوابش در لینک زیر به هر حال تخصصی هست و ممکنه به کار هر کسی نیاد ولی رویکرد کلیاش میتونه جالب باشه.
Hmm
و
Thanks!
گفتناش هم جالبه.
لینک سوال و جواب با ChatGPT
لینک سوال در mathoverflow
mathoverflow
تائو از
ChatGPT
کمک میگیره. میگه تا الان که باهاش کار کردم به hallucination و این چیزا برنخوردم(دست کم تا اون موقع)
میگه استراتژی کلیام اینه که هر چیزی رو گام به گام براش توضیح میدم و بعد از چک کردن جواب میرم مرحله بعد. این سوال و جوابش در لینک زیر به هر حال تخصصی هست و ممکنه به کار هر کسی نیاد ولی رویکرد کلیاش میتونه جالب باشه.
Hmm
و
Thanks!
گفتناش هم جالبه.
لینک سوال و جواب با ChatGPT
لینک سوال در mathoverflow
👍12
Mathematical Musings
Photo
ریچارد فاینمن افسانه ای یه مساله ای رو در زمینه تصمیم گیری بهینه، توی دست نوشته هاش، نوشته و یه راه حلی برای اون ارائه کرده. راز سر به مهری که حالا از اون رمز گشایی کردند. راه حل فاینمن بهینه بوده، اون رو تعمیم دادند و همین طور بررسی کردند که واقعا و در عمل ملت چه رفتاری از خودشون نشون می دن.
فاینمن با رفیقش می ره رستوران و همون ماجرای سفارش غذا رو به یه مساله ریاضی تبدیل می کنه.
فاینمن تمرکزش روی یه رستوران بود و در تعمیم مساله رستوران های یه شهر رو در نظر گرفتند.
هر رستوران یه ارزش ثابتی داره بین صفر و یک(توزیع یکنواخت) کِی می فهمید ارزشش چیه؟ یه بار غذا خورده باشید اونجا. یه فرد قراره چند روزی اونجا بره و در رستوران های شهر غذا بخوره، چطور تصمیم بگیره کدوم رستوران بره تا این مجموع مقادیر ارزش رستوران ها رو ماکزیمم کنه؟
طالب همین صورت مساله رو ببینه صدتا بدوبیراه به طراح سوال، حل کننده و... نثار می کنه، چنان فرض های ساده سازانه ای در همین چند خط وجود داره که عملا اون رو از واقعیت منفک می کنه. کیفیت غذای رستوران ممکنه تغییر کنه و ثابت نیست، یه مساله درباره انسان و غذا؟ این خودش پیچیده ترینِ مساله ها است! ولی در مورد این مساله به نظر طالب هم کاری نداریم.
این مساله از نوع همون مساله ای هست که به اون reply خورده و پست های قبل تر از اون.
منتها توی مساله فاینمن توزیع مشخصه، می تونید برگردید به رستوران و هدف انتخاب یه فرد نیست و باید مجموع رو max کنید.
سیاست بهینه برای اون مساله اینه که هر شب یه رستوران رو انتخاب کنی و بعد تحت شرایطی به یه گزینه خاص که رسیدی تا آخر همون رو انتخاب کنی و دیگه چیزی رو عوض نکنی(این می شه همون نقطه بهینه یا انتخاب نهایی، مثل انتخاب همسر، انتخاب خونه، ماشین و...)
روی ۲۵۲۰ تا آدم واقعی هم همین آزمایش رو انجام دادند و رفتارشون خیلی شبیه جواب نهایی فاینمن بوده.
https://www.pnas.org/doi/10.1073/pnas.2509612123
فاینمن با رفیقش می ره رستوران و همون ماجرای سفارش غذا رو به یه مساله ریاضی تبدیل می کنه.
فاینمن تمرکزش روی یه رستوران بود و در تعمیم مساله رستوران های یه شهر رو در نظر گرفتند.
هر رستوران یه ارزش ثابتی داره بین صفر و یک(توزیع یکنواخت) کِی می فهمید ارزشش چیه؟ یه بار غذا خورده باشید اونجا. یه فرد قراره چند روزی اونجا بره و در رستوران های شهر غذا بخوره، چطور تصمیم بگیره کدوم رستوران بره تا این مجموع مقادیر ارزش رستوران ها رو ماکزیمم کنه؟
طالب همین صورت مساله رو ببینه صدتا بدوبیراه به طراح سوال، حل کننده و... نثار می کنه، چنان فرض های ساده سازانه ای در همین چند خط وجود داره که عملا اون رو از واقعیت منفک می کنه. کیفیت غذای رستوران ممکنه تغییر کنه و ثابت نیست، یه مساله درباره انسان و غذا؟ این خودش پیچیده ترینِ مساله ها است! ولی در مورد این مساله به نظر طالب هم کاری نداریم.
این مساله از نوع همون مساله ای هست که به اون reply خورده و پست های قبل تر از اون.
منتها توی مساله فاینمن توزیع مشخصه، می تونید برگردید به رستوران و هدف انتخاب یه فرد نیست و باید مجموع رو max کنید.
سیاست بهینه برای اون مساله اینه که هر شب یه رستوران رو انتخاب کنی و بعد تحت شرایطی به یه گزینه خاص که رسیدی تا آخر همون رو انتخاب کنی و دیگه چیزی رو عوض نکنی(این می شه همون نقطه بهینه یا انتخاب نهایی، مثل انتخاب همسر، انتخاب خونه، ماشین و...)
روی ۲۵۲۰ تا آدم واقعی هم همین آزمایش رو انجام دادند و رفتارشون خیلی شبیه جواب نهایی فاینمن بوده.
https://www.pnas.org/doi/10.1073/pnas.2509612123
❤10👍8
Mathematical Musings
چند تا ریاضیدان که سال قبل در Leiden University دور هم جمع شده بودند، یه بیانیه دادند درباره ریاضیات و هوش مصنوعی. شاید بشه گفت یه بیانیه حرفه ای و حتی سیاسی. حتی IMU هم endorsed کرده ماجرا رو. می گن ما ارزش هایی داریم: اثبات ریاضی، مسئولیت پذیری نویسنده…
این هم راه افتاد، گفتند به بقیه کاری نداریم، ما از AI استفاده نمی کنیم.
نه برای انتخاب مساله، نه برای حل مساله، نه برای چک کردن اثبات، نه برای مرور ادبیات، نه برای تدریس، نه برای نوشتن و نه برای هیچی!
https://www.begin-proof.com/declaration
نه برای انتخاب مساله، نه برای حل مساله، نه برای چک کردن اثبات، نه برای مرور ادبیات، نه برای تدریس، نه برای نوشتن و نه برای هیچی!
https://www.begin-proof.com/declaration
🤣25👏12👎1
Mathematical Musings
Photo
تولد
Vladimir Voevodsky
هست.
پدر شاغل در
Russian Academy of Sciences
و مادر شیمیدان.
رفت به
Moscow State University
منتها نه عملکرد تحصیلی خوبی داشت و نه سر کلاسها حاضر میشد. اخراج شد!
آدمی خاص، مسیری خاص، با تاثیرات خاصتر.
سال ۱۹۹۲ دکتریاش رو از دانشگاه هاروارد گرفت، در حالی که نه درخواست پذیرش داده بود و نه مدرک دانشگاهی رسمی داشت. مستقلا چند مقاله منتشر کرده بود و همین کمکش کرد.
برگردیم به دوران لیسانس:
دانشجوی سال اول لیسانس که بود استادش یه مقاله از گروتندیک بهش میده که گروتندیک تازه نوشته بود. بعدها گفت: فرانسوی رو به عشق خوندن کارهای گروتندیک یاد گرفته(این متن ۶۰ صفحهای یکی از مهمترین کارهای گروتندیک بود و تازه دوران عزلت رو شروع کرده بود، که اون رو نوشت. یه بخشی از اون به موضوع نقاشیهای کودکان بود(البته مربوط به ریاضی میشه))
Algebraic geometry, Algebraic topology, Homotopy theory
زمینههای کاریاش بودند و تونست
Milnor conjecture
رو با ابزارهایی که معرفی کرد ثابت کنه.
فیلدز سال ۲۰۰۲ رو به خاطر کارهاش گرفت.
به خاطر مشکل قلبی در سال ۲۰۱۷ و سن ۵۱ سالگی درگذشت.
اواخر ۱۹۹۰ متوجه شد در یکی از مقالات خودش خطایی وجود داره. همین باعث شد نگاهش به اثبات سنتی متزلزل بشه. میگفت: من خطا کردم، داورها نفهمیدند، سالها خوانندهها هم نفهمیدند. پس چه چیزی تضمین میکنه که یک اثبات درسته؟
اعتقاد داشت بخشی از ریاضیات مدرن اونقدر پیچیده شده و اثباتها اونقدر طولانی شده که هیچکس دیگه در مقالات اثباتها رو خط به خط نمیخونه.
حملهاش به این باور قدیمی و چند هزار ساله ریاضیات بود: اگه اثبات داری، یقین داری! ولی Voevodsky میگفت: ما فقط فکر میکنیم اثبات داریم.
زمانی گفته بود: دارم ایمانم رو به سیستم داوری موجود برای بررسی مقالات از دست میدم.
اوائل رفت سراغ همین کارهای معمول
formal verification, proof assistant
بعدا احساس کرد همین هم کافی نیست. احساس کرد که شاید اصلا خود
foundation
ریاضی یعنی ZFC مشکل داره.
کامپیوتر رو مجبور کنیم زبون ریاضی بفهمه؟ شاید باید زبان ریاضیات رو عوض کنیم.
شاید بیربط نباشه که بگیم با دو تا
Voevodsky
روبرو هستیم.
Voevodsky I
که هندسه جبری و... کار میکرد و فیلدز گرفت.
Voevodsky II
که دنبال فرمالسازی و foundation ریاضیات رفت.
شاید خودش دومی رو مهمتر میدونست.
Vladimir Voevodsky
هست.
پدر شاغل در
Russian Academy of Sciences
و مادر شیمیدان.
رفت به
Moscow State University
منتها نه عملکرد تحصیلی خوبی داشت و نه سر کلاسها حاضر میشد. اخراج شد!
آدمی خاص، مسیری خاص، با تاثیرات خاصتر.
سال ۱۹۹۲ دکتریاش رو از دانشگاه هاروارد گرفت، در حالی که نه درخواست پذیرش داده بود و نه مدرک دانشگاهی رسمی داشت. مستقلا چند مقاله منتشر کرده بود و همین کمکش کرد.
برگردیم به دوران لیسانس:
دانشجوی سال اول لیسانس که بود استادش یه مقاله از گروتندیک بهش میده که گروتندیک تازه نوشته بود. بعدها گفت: فرانسوی رو به عشق خوندن کارهای گروتندیک یاد گرفته(این متن ۶۰ صفحهای یکی از مهمترین کارهای گروتندیک بود و تازه دوران عزلت رو شروع کرده بود، که اون رو نوشت. یه بخشی از اون به موضوع نقاشیهای کودکان بود(البته مربوط به ریاضی میشه))
Algebraic geometry, Algebraic topology, Homotopy theory
زمینههای کاریاش بودند و تونست
Milnor conjecture
رو با ابزارهایی که معرفی کرد ثابت کنه.
فیلدز سال ۲۰۰۲ رو به خاطر کارهاش گرفت.
به خاطر مشکل قلبی در سال ۲۰۱۷ و سن ۵۱ سالگی درگذشت.
اواخر ۱۹۹۰ متوجه شد در یکی از مقالات خودش خطایی وجود داره. همین باعث شد نگاهش به اثبات سنتی متزلزل بشه. میگفت: من خطا کردم، داورها نفهمیدند، سالها خوانندهها هم نفهمیدند. پس چه چیزی تضمین میکنه که یک اثبات درسته؟
اعتقاد داشت بخشی از ریاضیات مدرن اونقدر پیچیده شده و اثباتها اونقدر طولانی شده که هیچکس دیگه در مقالات اثباتها رو خط به خط نمیخونه.
حملهاش به این باور قدیمی و چند هزار ساله ریاضیات بود: اگه اثبات داری، یقین داری! ولی Voevodsky میگفت: ما فقط فکر میکنیم اثبات داریم.
زمانی گفته بود: دارم ایمانم رو به سیستم داوری موجود برای بررسی مقالات از دست میدم.
اوائل رفت سراغ همین کارهای معمول
formal verification, proof assistant
بعدا احساس کرد همین هم کافی نیست. احساس کرد که شاید اصلا خود
foundation
ریاضی یعنی ZFC مشکل داره.
کامپیوتر رو مجبور کنیم زبون ریاضی بفهمه؟ شاید باید زبان ریاضیات رو عوض کنیم.
شاید بیربط نباشه که بگیم با دو تا
Voevodsky
روبرو هستیم.
Voevodsky I
که هندسه جبری و... کار میکرد و فیلدز گرفت.
Voevodsky II
که دنبال فرمالسازی و foundation ریاضیات رفت.
شاید خودش دومی رو مهمتر میدونست.
❤16🔥8👎1
به مناسبت کتاب
The Proof in the code
افرادی مثل Kevin Buzzard و دیگران درباره اینکه formalize کردن در Lean چیه صحبت می کنند؟ و اینکه
how computer verification is changing the way mathematicians collaborate, build trust, and decide what counts as proof
صحبت می کنند.
و یه روز دیگه
about Lean from the inside: its origins, its design, and...
احتمالا بعدا در یوتیوب هم بذارند.
Thursday, June 11: The Mathematicians
Friday, June 12: The Builders
The Proof in the code
افرادی مثل Kevin Buzzard و دیگران درباره اینکه formalize کردن در Lean چیه صحبت می کنند؟ و اینکه
how computer verification is changing the way mathematicians collaborate, build trust, and decide what counts as proof
صحبت می کنند.
و یه روز دیگه
about Lean from the inside: its origins, its design, and...
احتمالا بعدا در یوتیوب هم بذارند.
Thursday, June 11: The Mathematicians
Friday, June 12: The Builders
👍6❤5
Mathematical Musings
Photo
Red noise
یا خطای قمارباز هم بهش میگن، به اون
regression towards a mean
هم میگن. یه چیزی دیروز یا اخیرا خیلی بالا رفته و پیش خودت میگی حالا وقتشه برعکس بشه. "سه تا بچه اول پسر بوده، پس بعدی دختره!"، "این ماه که قراره بچهام به دنیا بیاد آمار به دنیا اومدن پسرها زیاد بوده پس بچه من دختره"
The “pessimistic” interpretation of random events.
Blue noise
برعکسه نگاه قبلی هست. دیروز و پریروز و... بالا بوده پس فردا هم بالا میره.
Hot hand fallacy
هم بهش میگن.
The more “optimistic” interpretation of random events.
منتها بعضی میگن شاید در بعضی مواقع غلط هم نباشه. موفقیتهای فردا همیشه مستقل از موفقیتهای دیروز و روزهای قبل نیست.
هر چند در رویدادهای واقعا تصادفی باز هم یه خطا محسوب می شه.
White noise/True Randomness
تفسیری تا حدی رادیکال از تصادفی بودن رویدادها. اگه سکهای رو هزار بار پرتاب کنی و هر هزار بار شیر اومده باشه(هر چند خود این اتفاق احتمالش کمه) اگه دفعه ۱۰۰۱ ام پرتاب کنی، شانس شیر و خط با هم برابره. آینده ربطی به گذشته نداره و هر روز، روز دیگری است!
اقتصاددانی که در مقاله ازش صحبت میشه یعنی
Paul Samuelson
کسی هست که طالب بدترین بدوبیراهها رو نثارش کرده. اینها در اقتصاد ادعا داشتند که ما داریم کار علمی میکنیم چون ریاضی بلدیم، بهینهسازی بلدیم. بقیه مشغول روششناسی هستند. با این ادعا که اگر ریاضی بلدی، میتونی کار علمی بکنی. طالب میگه عین رفتار بعضی از این روانکارها که به منتقدهاشون برمیگردند میگن که با پدرت مشکل داشتی تو در بچگی!
طالب میگه اینها اقتصاددانیهایی هستند که با مدلهای قلابی از جهان، ما رو گرفتار خطا میکنند. میگه اینها دربهترین حالت باید میرفتند به قمارخانه ولی به مدد مثلا ریاضیاتی که بلد بودند رفتند به آکادمی.
https://www.cantorsparadise.com/paul-samuelsons-three-flavors-of-randomness-86c82eaf767a
یا خطای قمارباز هم بهش میگن، به اون
regression towards a mean
هم میگن. یه چیزی دیروز یا اخیرا خیلی بالا رفته و پیش خودت میگی حالا وقتشه برعکس بشه. "سه تا بچه اول پسر بوده، پس بعدی دختره!"، "این ماه که قراره بچهام به دنیا بیاد آمار به دنیا اومدن پسرها زیاد بوده پس بچه من دختره"
The “pessimistic” interpretation of random events.
Blue noise
برعکسه نگاه قبلی هست. دیروز و پریروز و... بالا بوده پس فردا هم بالا میره.
Hot hand fallacy
هم بهش میگن.
The more “optimistic” interpretation of random events.
منتها بعضی میگن شاید در بعضی مواقع غلط هم نباشه. موفقیتهای فردا همیشه مستقل از موفقیتهای دیروز و روزهای قبل نیست.
هر چند در رویدادهای واقعا تصادفی باز هم یه خطا محسوب می شه.
White noise/True Randomness
تفسیری تا حدی رادیکال از تصادفی بودن رویدادها. اگه سکهای رو هزار بار پرتاب کنی و هر هزار بار شیر اومده باشه(هر چند خود این اتفاق احتمالش کمه) اگه دفعه ۱۰۰۱ ام پرتاب کنی، شانس شیر و خط با هم برابره. آینده ربطی به گذشته نداره و هر روز، روز دیگری است!
اقتصاددانی که در مقاله ازش صحبت میشه یعنی
Paul Samuelson
کسی هست که طالب بدترین بدوبیراهها رو نثارش کرده. اینها در اقتصاد ادعا داشتند که ما داریم کار علمی میکنیم چون ریاضی بلدیم، بهینهسازی بلدیم. بقیه مشغول روششناسی هستند. با این ادعا که اگر ریاضی بلدی، میتونی کار علمی بکنی. طالب میگه عین رفتار بعضی از این روانکارها که به منتقدهاشون برمیگردند میگن که با پدرت مشکل داشتی تو در بچگی!
طالب میگه اینها اقتصاددانیهایی هستند که با مدلهای قلابی از جهان، ما رو گرفتار خطا میکنند. میگه اینها دربهترین حالت باید میرفتند به قمارخانه ولی به مدد مثلا ریاضیاتی که بلد بودند رفتند به آکادمی.
https://www.cantorsparadise.com/paul-samuelsons-three-flavors-of-randomness-86c82eaf767a
❤6🔥4
Mathematical Musings
Photo
خانم Carina اینجا یه صحبت ۱۵ دقیقهای در مورد
Frontiers of AI
برای تحقیقات ریاضی انجام میدن.
میگن Axiom یه شرکت ۴۰ تا ۴۵ نفره هست. میگن این بازی AI برای math از مسائل المپیاد شروع شد. ۲۸ از ۴۲ شد و نقره گرفت و کمی با gold medal فاصله داشت. شرکتهای دیگه رو مثال میزنه که هی رشد کردند و موفقیتهای بیشتر به دست آوردند. از موفقیت خیرهکننده Axiom در مسابقات پاتنام میگه(سختترین مسابقه ریاضی در سطح لیسانس)
میگه موفقیتها در سطح Olympiad داشت عالی پیش میرفت که ما این سوال رو از خودمون پرسیدیم:
What about...mathematical research?
میگه سوال اینه اصلا چرا رفتیم سراغ math؟ چون ریاضی پایه است واسه همه علوم دیگه. باید زمین بازی رو آماده کنیم. فیزیک، شیمی، نوروساینس همه وابسته ریاضیات هستند. میگه frankly بگم: ریاضیات توی تمام علوم کاربردی استفاده میشه و به همین خاطر رفتیم سراغش.
میگه ریاضیات المپیاد خیلی سخت نبود، کلی استاد، دانشجو، coach، نمونه سوال، بنچمارک داشتیم و میتونستیم از اونا استفاده کنیم.
میگه یه private benchmark تهیه شد و قرار شد روی اون کار بشه.
از شرکت خودش میگه که از ابتدای سال چند تا مقاله رو در Arxiv منتشر کردند و سه تا هم در ژورنالهای ریاضی منتشر شده.
مقالاتی در حوزههای زیر: نظریه اعداد، جبر جابهجایی و هندسه جبری.
بخش دوم حرفاش درباره دو مقاله است. یکی در نظریه جبری اعداد و یکی هم این.
یه جاهایی خیلی تند حرف میزنه.
https://youtu.be/WMo-RmSJQpE?is=4bs0yPGFciMS2cWe
Frontiers of AI
برای تحقیقات ریاضی انجام میدن.
میگن Axiom یه شرکت ۴۰ تا ۴۵ نفره هست. میگن این بازی AI برای math از مسائل المپیاد شروع شد. ۲۸ از ۴۲ شد و نقره گرفت و کمی با gold medal فاصله داشت. شرکتهای دیگه رو مثال میزنه که هی رشد کردند و موفقیتهای بیشتر به دست آوردند. از موفقیت خیرهکننده Axiom در مسابقات پاتنام میگه(سختترین مسابقه ریاضی در سطح لیسانس)
میگه موفقیتها در سطح Olympiad داشت عالی پیش میرفت که ما این سوال رو از خودمون پرسیدیم:
What about...mathematical research?
میگه سوال اینه اصلا چرا رفتیم سراغ math؟ چون ریاضی پایه است واسه همه علوم دیگه. باید زمین بازی رو آماده کنیم. فیزیک، شیمی، نوروساینس همه وابسته ریاضیات هستند. میگه frankly بگم: ریاضیات توی تمام علوم کاربردی استفاده میشه و به همین خاطر رفتیم سراغش.
میگه ریاضیات المپیاد خیلی سخت نبود، کلی استاد، دانشجو، coach، نمونه سوال، بنچمارک داشتیم و میتونستیم از اونا استفاده کنیم.
میگه یه private benchmark تهیه شد و قرار شد روی اون کار بشه.
از شرکت خودش میگه که از ابتدای سال چند تا مقاله رو در Arxiv منتشر کردند و سه تا هم در ژورنالهای ریاضی منتشر شده.
مقالاتی در حوزههای زیر: نظریه اعداد، جبر جابهجایی و هندسه جبری.
بخش دوم حرفاش درباره دو مقاله است. یکی در نظریه جبری اعداد و یکی هم این.
یه جاهایی خیلی تند حرف میزنه.
https://youtu.be/WMo-RmSJQpE?is=4bs0yPGFciMS2cWe
❤6
Mathematical Musings
این نتیجه هم در نظریه اعداد ظاهرا result مهمی بوده. یه نتیجه که فقط و فقط کار انسان بوده. https://arxiv.org/abs/2605.28781
اون حدس
sum-product
که توسط انسان اثبات شد، بعد اومدند به
GPT-5.5
گفتند برو یه اثبات برای این حدس پیدا کن(در واقع یه disproof)
خود این ریاضیدانهایی که این حدس رو اثبات کردند از اون مساله معروف اردوش که توسط AI حل شد یعنی
unit distance
ایده گرفتند. اینجا هم به ChatGPT گفتند برو اون اثبات رو بخون و سعی کن این حدس sum-product رو رد کنی.
چند وقت پیش یه پیشنهادی دادند که خیلی جالب بود. گفتند که هر مقالهای که میخواد منتشر بشه، مقالهای که کار خود انسان هست یه
Kolmogorov Appendix
براش تهیه بشه.
از مدل بخواین که نتایجی که شما بدست آوردین رو recover کنه و بعد ته مقاله
minimal prompt
که برای رسیدن به اون استفاده شده، ذکر بشه.
لینک مربوط به سوال و جواب با ChatGPT
sum-product
که توسط انسان اثبات شد، بعد اومدند به
GPT-5.5
گفتند برو یه اثبات برای این حدس پیدا کن(در واقع یه disproof)
خود این ریاضیدانهایی که این حدس رو اثبات کردند از اون مساله معروف اردوش که توسط AI حل شد یعنی
unit distance
ایده گرفتند. اینجا هم به ChatGPT گفتند برو اون اثبات رو بخون و سعی کن این حدس sum-product رو رد کنی.
چند وقت پیش یه پیشنهادی دادند که خیلی جالب بود. گفتند که هر مقالهای که میخواد منتشر بشه، مقالهای که کار خود انسان هست یه
Kolmogorov Appendix
براش تهیه بشه.
از مدل بخواین که نتایجی که شما بدست آوردین رو recover کنه و بعد ته مقاله
minimal prompt
که برای رسیدن به اون استفاده شده، ذکر بشه.
لینک مربوط به سوال و جواب با ChatGPT
❤11🤣3
Mathematical Musings
از حدود چند دهه پیش یه سری اثبات از CS وارد ریاضی شد که بعضی هاشون خیلی بحث برانگیز شدند. نوعی از اثبات ها که با مفهومی که همه از اثبات در ریاضی می دونند فرق داره. Zero-knowledge proof probabilistically checkable proofs و چند نوع دیگه. تمام این اثبات ها probabilistic…
ظاهرا چند هفته پیش
Michael O. Rabin
هم درگذشت.
در واقع باید گفت بیشتر یه CS کار بود و برنده جایزه تورینگ ۱۹۷۶. جایزه رو به خاطر کارهاش در
computational complexity
گرفت.
ریاضیدان و set theorist معروف
Saharon Shelah
شاگردش بوده.
در نوجوانی به ریاضیات علاقه مند شد و پدرش اون رو به بهترین مدرسه فرستاد و اونجا زیر نظر
Elisha Netanyahu
ریاضیدان، آموزش دید.
جایزه رو به طور مشترک با Dana Scott گرفت.
ظاهرا CS کارها در حال تهیه یه متن طولانی و فنی در ستایش خودش و کارهاش هستند.
https://rjlipton.com/2026/04/22/rabin-has-just-passed-away/
Michael O. Rabin
هم درگذشت.
در واقع باید گفت بیشتر یه CS کار بود و برنده جایزه تورینگ ۱۹۷۶. جایزه رو به خاطر کارهاش در
computational complexity
گرفت.
ریاضیدان و set theorist معروف
Saharon Shelah
شاگردش بوده.
در نوجوانی به ریاضیات علاقه مند شد و پدرش اون رو به بهترین مدرسه فرستاد و اونجا زیر نظر
Elisha Netanyahu
ریاضیدان، آموزش دید.
جایزه رو به طور مشترک با Dana Scott گرفت.
For their joint paper "Finite Automata and Their Decision Problems," which introduced the idea of nondeterministic machines, which has proved to be an enormously valuable concept. Their (Scott & Rabin) [sic] classic paper has been a continuous source of inspiration for subsequent work in this field.می گن کارهاش در قلب ریاضیات و CS قرار داره و میراثش در این حوزه ها مثل یه معدن غنی می مونه.
ظاهرا CS کارها در حال تهیه یه متن طولانی و فنی در ستایش خودش و کارهاش هستند.
https://rjlipton.com/2026/04/22/rabin-has-just-passed-away/
❤9👌3
Mathematical Musings
قضیه دوم ناتمامیت گودل رو هم با Claude تونستند autoformalisation کنند. ۵۰ هزار خط کد. ظاهرا اتفاقی که افتاده و جالب هست اینه که رفتند سراغ یه مقاله ای که کار رو شروع کنند و جلو هم رفتند بعد دیدند این چیزی که بهش رسیدیم ربطی به قضیه گودل نداره. مشکل چی بوده؟…
اثبات متداول اصم بودن رادیکال دو.
این ایرادها به اون وارده:
چرا میشه به صورت دو تا کسر نوشت، تعریف گویا بودن چیه؟ اون بحث
common divisor
که اصلا برای کسانی که اولین بار اثبات رو میبینند هم تا حدی سواله.
اینکه توان دوم چیزی زوج باشه، خودش هم زوج هست باید قبلا بررسی بشه.
اون قسمت که
n√2 = m
پس داریم:
2n^2 = m^2
برای انسان صفر ثانیه هم طول نمی کشه ولی باید بررسی بشه.
خود اون مقاله رو پیدا نکردم ولی این چند تا بود. این البته فقط مسائلی هست که در خود اثبات وجود داره. اینکه 2√ خودش مثلا می شه sup یه مجموعه ای و...بقیه ماجرا است.
اینکه طرف اومده به خاطر فرمالایز کردن FLT ۹ میلیون دلار گرنت گرفته به خاطر همین چیزها است(البته نه فقط برای FLT)
این ایرادها به اون وارده:
چرا میشه به صورت دو تا کسر نوشت، تعریف گویا بودن چیه؟ اون بحث
common divisor
که اصلا برای کسانی که اولین بار اثبات رو میبینند هم تا حدی سواله.
اینکه توان دوم چیزی زوج باشه، خودش هم زوج هست باید قبلا بررسی بشه.
اون قسمت که
n√2 = m
پس داریم:
2n^2 = m^2
برای انسان صفر ثانیه هم طول نمی کشه ولی باید بررسی بشه.
خود اون مقاله رو پیدا نکردم ولی این چند تا بود. این البته فقط مسائلی هست که در خود اثبات وجود داره. اینکه 2√ خودش مثلا می شه sup یه مجموعه ای و...بقیه ماجرا است.
اینکه طرف اومده به خاطر فرمالایز کردن FLT ۹ میلیون دلار گرنت گرفته به خاطر همین چیزها است(البته نه فقط برای FLT)
🔥3❤2