یه حدس اردوش رو بررسی می کنند، در زمینه نظریه گراف.
از AI کمک می گیرند تا مثال هایی ارائه بدند که log concave نباشند.
دو نکته جالب ارائه اش داشت:
چند جا توسط حضار سوالاتی از ارائه دهنده پرسیده می شه که کمی چالشی هست و جواب رو دقیق نمی دونست، طرفین با این مساله عادی برخورد می کنند.
یه موضوعی رو برای tree ها تا ۲۵ راس با کمک کامپیوتر بررسی می کنند و می بینند درسته، توی سال ۲۰۲۳ ثابت می کنند برای tree های با ۲۶ راس fail می شه! که همین موضوع برای یکی از حضار جالب می شه، می پرسه چطور اون بررسی اولیه تا ۲۵ ادامه پیدا کرد و ۲۶ رو بررسی نکردند؟
https://youtu.be/5yZ1D5MEM_M?si=Ul0n4GjNxjOJU9sK
از AI کمک می گیرند تا مثال هایی ارائه بدند که log concave نباشند.
دو نکته جالب ارائه اش داشت:
چند جا توسط حضار سوالاتی از ارائه دهنده پرسیده می شه که کمی چالشی هست و جواب رو دقیق نمی دونست، طرفین با این مساله عادی برخورد می کنند.
یه موضوعی رو برای tree ها تا ۲۵ راس با کمک کامپیوتر بررسی می کنند و می بینند درسته، توی سال ۲۰۲۳ ثابت می کنند برای tree های با ۲۶ راس fail می شه! که همین موضوع برای یکی از حضار جالب می شه، می پرسه چطور اون بررسی اولیه تا ۲۵ ادامه پیدا کرد و ۲۶ رو بررسی نکردند؟
https://youtu.be/5yZ1D5MEM_M?si=Ul0n4GjNxjOJU9sK
🔥5🆒4
“Not every obvious statement is true.”
این مقاله جالب بود، به این سوال جواب می ده که چرا ما به دنبال formalize کردن قضیه های ریاضی هستیم و چرا نمی ریم به جاش catching کنیم error ها رو.
اول خودش می گه که من ریاضی، کامپیوتر و پازل بازی رو دوست دارم. می گه این کار یعنی فرمالایز کردن قضیه ها این سه تا رو با هم به من می ده.
می گه از کتاب آنالیز تائو دارم توی Lean اثبات قضیه ها رو فرمالایز می کنم.
اول اینکه می گه با Lean می تونیم امکانات ابتدایی یه IDE رو داشته باشیم.
می گه می تونیم وابستگی و ارتباط بین قضیه ها رو پیدا کنیم و گراف شون رو داشته باشیم.
می گه الان اگر یکی گفت فلان قضیه یا مثال غلطه هیچ تضمینی نیست بقیه که به اون ارجاع دادند یا کارشون متکی هست، خبردار بشند. می گه با Lean می تونیم وابستگی ها رو مدیریت کنیم.
یه بخشی هم در رابطه با TypeScript توضیح داده.
https://rkirov.github.io/posts/why_lean/
این مقاله جالب بود، به این سوال جواب می ده که چرا ما به دنبال formalize کردن قضیه های ریاضی هستیم و چرا نمی ریم به جاش catching کنیم error ها رو.
اول خودش می گه که من ریاضی، کامپیوتر و پازل بازی رو دوست دارم. می گه این کار یعنی فرمالایز کردن قضیه ها این سه تا رو با هم به من می ده.
می گه از کتاب آنالیز تائو دارم توی Lean اثبات قضیه ها رو فرمالایز می کنم.
اول اینکه می گه با Lean می تونیم امکانات ابتدایی یه IDE رو داشته باشیم.
می گه می تونیم وابستگی و ارتباط بین قضیه ها رو پیدا کنیم و گراف شون رو داشته باشیم.
می گه الان اگر یکی گفت فلان قضیه یا مثال غلطه هیچ تضمینی نیست بقیه که به اون ارجاع دادند یا کارشون متکی هست، خبردار بشند. می گه با Lean می تونیم وابستگی ها رو مدیریت کنیم.
یه بخشی هم در رابطه با TypeScript توضیح داده.
https://rkirov.github.io/posts/why_lean/
❤6🆒4👍3
امروز سالروز مرگ تارسکی بود.
در موردش می گند کسانی که حتی زمینه قوی در ریاضی یا منطق داشتند، درک نوشته ها و آثارش براشون راحت نبوده.
پارادوکس معروف باناخ تارسکی می گه یه کره سه بعدی رو می شه به قطعاتی تقسیم کرد و بعد دوباره طوری سر هم کرد که دو کره ازش به دست بیاد.
برای این کار نیاز به اصل انتخاب داریم و همین پارادوکس یکی از دلایل حمله مخالفان به این اصل هست.
از اون طرف طرفدارای این اصل می گند این تناقض بیشتر از اینکه به این اصل برگرده به خاطر ماهیت و پیچیدگی مفهوم بی نهایت هست.
حتی بدون این اصل هم سروکله زدن با مفهوم بی نهایت دردسرهای خودش رو داره.
در موردش می گند کسانی که حتی زمینه قوی در ریاضی یا منطق داشتند، درک نوشته ها و آثارش براشون راحت نبوده.
پارادوکس معروف باناخ تارسکی می گه یه کره سه بعدی رو می شه به قطعاتی تقسیم کرد و بعد دوباره طوری سر هم کرد که دو کره ازش به دست بیاد.
برای این کار نیاز به اصل انتخاب داریم و همین پارادوکس یکی از دلایل حمله مخالفان به این اصل هست.
از اون طرف طرفدارای این اصل می گند این تناقض بیشتر از اینکه به این اصل برگرده به خاطر ماهیت و پیچیدگی مفهوم بی نهایت هست.
حتی بدون این اصل هم سروکله زدن با مفهوم بی نهایت دردسرهای خودش رو داره.
❤18👌6👍2🔥2
آقای
Kenji Fukaya
ریاضیدان ۶۶ ساله ژاپنی. زمینه کاری شون
symplectic topology
هست. مفهوم
Fukaya category
در ریاضی به اسم ایشون هست.
اخیرا جایزه
Shaw Prize
رو بردند که به نوبل شرق معروفه.
از سال ۲۰۰۴ این جایزه رو می دند. مقدار جایزه ۱.۲ میلیون دلار هست.
جایزه در زمینه های زیر داده می شه: نجوم، پزشکی، ریاضی.
قبلا در ریاضی افرادی مثل:
Peter Sarnak, Michel Talagrand,
Richard S. Hamilton, Vladimir Arnold,
David Mumford, Shiing-Shen Chern
جایزه رو بردند. جمله ای که پشت مدال نوشته شده اینه:
قانون طبیعت را درک کنید و از آن استفاده کنید.
Kenji Fukaya
ریاضیدان ۶۶ ساله ژاپنی. زمینه کاری شون
symplectic topology
هست. مفهوم
Fukaya category
در ریاضی به اسم ایشون هست.
اخیرا جایزه
Shaw Prize
رو بردند که به نوبل شرق معروفه.
از سال ۲۰۰۴ این جایزه رو می دند. مقدار جایزه ۱.۲ میلیون دلار هست.
جایزه در زمینه های زیر داده می شه: نجوم، پزشکی، ریاضی.
قبلا در ریاضی افرادی مثل:
Peter Sarnak, Michel Talagrand,
Richard S. Hamilton, Vladimir Arnold,
David Mumford, Shiing-Shen Chern
جایزه رو بردند. جمله ای که پشت مدال نوشته شده اینه:
قانون طبیعت را درک کنید و از آن استفاده کنید.
❤16👎2
Mathematical Musings
Photo
دو تا تاس هم اندازه در نظر بگیرید، ممکنه که تو یکی سوراخی ایجاد کنید که بتونید اون یکی تاس رو ازش عبور بدید؟
احتمالا می گید: نه.
این سوال به چند قرن قبل برمی گرده، ۱۶۹۳، دوران جان والیس ریاضیدان. جواب والیس به این سوال مثبت بود.
دیگه برای چه شکل هایی می شه مساله رو بررسی کرد، به دلایل ریاضی بهتره بریم سراغ اشکال محدب، یعنی چند وجهی های محدب.
در سال ۱۹۶۸ ثابت شد که چهار وجهی و هشت وجهی هم این خاصیت رو دارند.
به این مسیرها یا تونل ها اصطلاحا می گند:
Rupert tunnels
حدس کلی: همه چند وجهی های محدب این خاصیت رو دارند.
تا اینکه چند ماه پیش یه مقاله منتشر کردند و یه شکل با ۹۰ راس و ۱۵۲ تا وجه ساختند که این خاصیت رو نداشت.
دو تا دوست که از نوجوانی با هم بودند و عاشق ریاضیات و الان یکی مدرک دکتری داره و یکی ارشد(و هیچ کدوم در دانشگاه فعال نیستند) تونستند این کار رو انجام بدند.
چطور به این مساله علاقه مند شدند؟
با دیدن یه ویدئو در یوتیوب!
توی یه پایگاه داده از شکل های محدب جستجو کردند تا برای اون حدس یه مثال نقض پیدا کنند که پیدا نشد. تصمیم گرفتند خودشون یه شکلی بسازند.
در مورد خودشون می گند:
لینک مقاله کوانتا:
https://www.quantamagazine.org/first-shape-found-that-cant-pass-through-itself-20251024/
لینک یه ویدئو که نشون می ده چطور یه مکعب رو می شه از اون یکی عبور داد:
https://youtu.be/D-W2QMSXSG4?si=tBOiHx6JyW_ZkMQR
احتمالا می گید: نه.
این سوال به چند قرن قبل برمی گرده، ۱۶۹۳، دوران جان والیس ریاضیدان. جواب والیس به این سوال مثبت بود.
دیگه برای چه شکل هایی می شه مساله رو بررسی کرد، به دلایل ریاضی بهتره بریم سراغ اشکال محدب، یعنی چند وجهی های محدب.
در سال ۱۹۶۸ ثابت شد که چهار وجهی و هشت وجهی هم این خاصیت رو دارند.
به این مسیرها یا تونل ها اصطلاحا می گند:
Rupert tunnels
حدس کلی: همه چند وجهی های محدب این خاصیت رو دارند.
تا اینکه چند ماه پیش یه مقاله منتشر کردند و یه شکل با ۹۰ راس و ۱۵۲ تا وجه ساختند که این خاصیت رو نداشت.
دو تا دوست که از نوجوانی با هم بودند و عاشق ریاضیات و الان یکی مدرک دکتری داره و یکی ارشد(و هیچ کدوم در دانشگاه فعال نیستند) تونستند این کار رو انجام بدند.
چطور به این مساله علاقه مند شدند؟
با دیدن یه ویدئو در یوتیوب!
توی یه پایگاه داده از شکل های محدب جستجو کردند تا برای اون حدس یه مثال نقض پیدا کنند که پیدا نشد. تصمیم گرفتند خودشون یه شکلی بسازند.
در مورد خودشون می گند:
We’re just humble mathematicians
لینک مقاله کوانتا:
https://www.quantamagazine.org/first-shape-found-that-cant-pass-through-itself-20251024/
لینک یه ویدئو که نشون می ده چطور یه مکعب رو می شه از اون یکی عبور داد:
https://youtu.be/D-W2QMSXSG4?si=tBOiHx6JyW_ZkMQR
❤19🤔3👎1
Mathematical Musings
دو تا تاس هم اندازه در نظر بگیرید، ممکنه که تو یکی سوراخی ایجاد کنید که بتونید اون یکی تاس رو ازش عبور بدید؟ احتمالا می گید: نه. این سوال به چند قرن قبل برمی گرده، ۱۶۹۳، دوران جان والیس ریاضیدان. جواب والیس به این سوال مثبت بود. دیگه برای چه شکل هایی می…
این اون چیزیه که ساختند، دو تا از اینا اگر داشته باشید نمی تونید تو یکی حفره ایجاد کنید طوری که اون یکی ازش رد بشه.
اون نفر سمت چپ اسمش
Sergey Yurkevich
هست، همونیه که دکتری داره.
دو تا لیسانس داره، دو تا فوق لیسانس.
پروژه با R زده، بازی هم ساخته و...
اون نفر سمت چپ اسمش
Sergey Yurkevich
هست، همونیه که دکتری داره.
دو تا لیسانس داره، دو تا فوق لیسانس.
پروژه با R زده، بازی هم ساخته و...
❤14🆒4🤣1
Forwarded from Linuxor ?
قدرت DeepSeek-OCR رو ببینید !
این یه نامه به شدت ناخواناس که یه ریاضی دان سال 1913 نوشتش و دیپ سیک تونسته بخونتش
از اینجا میتونید خودتون تستش کنید :
www.alphaxiv.org/models/deepseek/deepseek-ocr
@Linuxor ~ Deedy
این یه نامه به شدت ناخواناس که یه ریاضی دان سال 1913 نوشتش و دیپ سیک تونسته بخونتش
از اینجا میتونید خودتون تستش کنید :
www.alphaxiv.org/models/deepseek/deepseek-ocr
@Linuxor ~ Deedy
❤18👏3👎2
Mathematical Musings
“Not every obvious statement is true.” این مقاله جالب بود، به این سوال جواب می ده که چرا ما به دنبال formalize کردن قضیه های ریاضی هستیم و چرا نمی ریم به جاش catching کنیم error ها رو. اول خودش می گه که من ریاضی، کامپیوتر و پازل بازی رو دوست دارم. می گه این…
راسل اگر زنده بود حتما از Lean استفاده می کرد، هر چند به نظر می رسه Lean یه جاهایی از راسل عقب هست!
🤣20