Mathematical Musings
مرگ یک Algebraic topologist ریاضیدان آمریکایی Jack Morava درگذشت. ظاهرا پدرومادرش نقش زیادی در ایجاد علاقه اش به توپولوژی داشتند(توضیحات بیشتری جایی ندیدم) اول فیزیک خوند و بعد رفت به سمت ریاضی. بهش ریاضیدان ریاضیدان ها هم می گفتند. ظاهرا شخصیت شوخ طبع…
وقتی نویسنده نسبت به سنگینی بحث آگاه هست و سعی می کنه با یه شوخی وارد بحث اصلی بشه.
به جای جواب دادن به سوالات وجودی که کار فلسفه است، حالا که می دونیم چیزهایی وجود داره بیایم دسته بندی شون کنیم.
به جای جواب دادن به سوالات وجودی که کار فلسفه است، حالا که می دونیم چیزهایی وجود داره بیایم دسته بندی شون کنیم.
❤17👏4
Mathematical Musings
In any sequence of (n² + 1) distinct integers, there exists either an increasing or a decreasing subsequence of length (n +1).
If you drop a map of your country on the floor, there will be a point on the map that touches the actual point it refers to.
Brouwer's fixed point theorem .
🔥42❤5👏4🆒3
ظاهرا در فیزیک هم داره این کار متداول می شه:
formal verification
این دفعه در فیزیک کوانتوم، یه قضیه ای که اثبات اصلی اش gap داشته رو و بعدا اثبات اصلاح شده ای براش پیدا شده، توی Lean نوشتند.
طبیعتا من از خود قضیه و چند و چونش سر در نمیارم ولی این طور که مدعی شده
the most technically demanding theorem in physics with a computer-verified proof to date...
هست.
در حین این کار توی اثبات اصلاح شده چند تا ابهام و ایراد رو برطرف کردند و یه کتابخونه در Lean ایجاد کردند.
پ ن: حالا من به طور کلی در این زمینه صاحب نظر نیستم و نمی دونم چقدر کار چالشی یا سختی می تونه باشه، ولی با توجه به گسترش این موضوع به نظرم مقاله بازان و مقاله سازان وطنی و... بهتره از این فرمال سازی قضایا غافل نشند، مجلاتی هست که شما اگر قضایای رودین رو هم فرمال سازی کنی چاپش کنند!
لینک مقاله
formal verification
این دفعه در فیزیک کوانتوم، یه قضیه ای که اثبات اصلی اش gap داشته رو و بعدا اثبات اصلاح شده ای براش پیدا شده، توی Lean نوشتند.
طبیعتا من از خود قضیه و چند و چونش سر در نمیارم ولی این طور که مدعی شده
the most technically demanding theorem in physics with a computer-verified proof to date...
هست.
در حین این کار توی اثبات اصلاح شده چند تا ابهام و ایراد رو برطرف کردند و یه کتابخونه در Lean ایجاد کردند.
پ ن: حالا من به طور کلی در این زمینه صاحب نظر نیستم و نمی دونم چقدر کار چالشی یا سختی می تونه باشه، ولی با توجه به گسترش این موضوع به نظرم مقاله بازان و مقاله سازان وطنی و... بهتره از این فرمال سازی قضایا غافل نشند، مجلاتی هست که شما اگر قضایای رودین رو هم فرمال سازی کنی چاپش کنند!
لینک مقاله
👍10❤7👏5
تعریف دنباله کشی رو احتمالا همه با اون آشنایی دارند، منتها این تعریف یه تعریف معادل دیگه هم داره که احتمالا خیلی ها ندیدند(خودم هم تازه دیدم)
∀ε>0, ∃n, ∀s≥n |x_s − x_n| < ε
عجیب که کسی هم به اون اشاره نکرده یا من ندیده بودم.
می گند اون تعریفی که معروف تره، شهودی تره.
اینجا در موردش نوشته:
https://math.stackexchange.com/questions/1818520/definition-of-cauchy-sequence
∀ε>0, ∃n, ∀s≥n |x_s − x_n| < ε
عجیب که کسی هم به اون اشاره نکرده یا من ندیده بودم.
می گند اون تعریفی که معروف تره، شهودی تره.
اینجا در موردش نوشته:
https://math.stackexchange.com/questions/1818520/definition-of-cauchy-sequence
✍9❤4🔥2👌2
Mathematical Musings
ظاهرا در فیزیک هم داره این کار متداول می شه: formal verification این دفعه در فیزیک کوانتوم، یه قضیه ای که اثبات اصلی اش gap داشته رو و بعدا اثبات اصلاح شده ای براش پیدا شده، توی Lean نوشتند. طبیعتا من از خود قضیه و چند و چونش سر در نمیارم ولی این طور که مدعی…
دوستان می گند:
ریاضی در کتاب های درسی بیشتر در سطح ایده های اولیه نوشته شده.
اثبات بالا از کتاب رودین هست که ثابت می کنه عدد رادیکال 2 یه عدد گویا نیست، حتی همین اثبات ساده هم اونقدر سرراست و دقیق نیست که بشه خیلی راحت رسمی سازی کرد اون رو.
چیزهایی در زبان طبیعی پنهان شده که در تعامل دو تا آدم که دارند ریاضی می خونند و با اون زبان با هم حرف می زنند، گفتنش ضرورتی نداره. اما در فرمال سازی باید تکلیفش مشخص بشه. چرا در اثبات بالا می تونیم m و n رو طوری انتخاب کنیم که زوج نباشند؟ چرا چیزی اگه زوج نباشه به شکل 2k+1 می شه؟
ظاهرا باید هی و هی همه چیز رو decompose کرد و میزان جزئیات این کار بستگی به این داره که چه چیزهایی از قبل وجود داره و Solver چقدر پیشرفته هست.
ریاضی در کتاب های درسی بیشتر در سطح ایده های اولیه نوشته شده.
اثبات بالا از کتاب رودین هست که ثابت می کنه عدد رادیکال 2 یه عدد گویا نیست، حتی همین اثبات ساده هم اونقدر سرراست و دقیق نیست که بشه خیلی راحت رسمی سازی کرد اون رو.
چیزهایی در زبان طبیعی پنهان شده که در تعامل دو تا آدم که دارند ریاضی می خونند و با اون زبان با هم حرف می زنند، گفتنش ضرورتی نداره. اما در فرمال سازی باید تکلیفش مشخص بشه. چرا در اثبات بالا می تونیم m و n رو طوری انتخاب کنیم که زوج نباشند؟ چرا چیزی اگه زوج نباشه به شکل 2k+1 می شه؟
ظاهرا باید هی و هی همه چیز رو decompose کرد و میزان جزئیات این کار بستگی به این داره که چه چیزهایی از قبل وجود داره و Solver چقدر پیشرفته هست.
👍15❤5
Forwarded from ویتگنشتاین، زبان، زندگی و فلسفه (Formula)
«هیچکس نمیتواند ما را از بهشتی که کانتور برایمان ساخته، بیرون براند».
/دیوید هیلبرت
«من هرگز به فکر بیرون راندن کسی از این بهشت نمیافتم. کاری که میکنم متفاوت است: سعی میکنم به شما نشان دهم که این بهشت نیست _ تا هر کس بخواهد، داوطلبانه خودش کنار بکشد و از آن بیرون رود. میگویم: خوش آمدید؛ اما فقط اطرافتان را نگاهی بیندازید… (اگر یکی میتواند آن را بهشت ببیند، دیگری چرا نتواند آن را شوخی بداند؟»
ویتگنشتاین/ درسگفتارهای ویتگنشتاین در باب بنیادهای ریاضیات 1939. P 103
/دیوید هیلبرت
«من هرگز به فکر بیرون راندن کسی از این بهشت نمیافتم. کاری که میکنم متفاوت است: سعی میکنم به شما نشان دهم که این بهشت نیست _ تا هر کس بخواهد، داوطلبانه خودش کنار بکشد و از آن بیرون رود. میگویم: خوش آمدید؛ اما فقط اطرافتان را نگاهی بیندازید… (اگر یکی میتواند آن را بهشت ببیند، دیگری چرا نتواند آن را شوخی بداند؟»
ویتگنشتاین/ درسگفتارهای ویتگنشتاین در باب بنیادهای ریاضیات 1939. P 103
❤20🤣6
جناب تائو می گه مهمترین مزیت AI در ریاضیات مربوط به حل مسائل خیلی سخت نیست، بلکه استفاده از اون ها در حل مسائل زمان بر هست. می گه در این حالت خروجی یه AI همون چیزیه که یه انسان هم می تونه انجام بده ولی با صرف زمان بیشتر، ولی خود این نکته نقص نیست، یه مزیته، چون قابل بررسی توسط انسان هست.
می گه نمونه اش literature review هست، وقتی روی یه مساله معروف کار می کنی، مرور ادبیات سخت نیست، خود پژوهشگر می تونه کارو پیش ببره، ولی وقتی مساله منابع کم و یا پراکنده ای داره، پیدا کردن منابع سخت و طاقت فرسا است.
یه مثال می زنه در مورد سایت
https://www.erdosproblems.com/
می گه بالای هزارتا مساله از اردوش توش هست که حدود ۶۰۰ تا حل نشده است، بعضی هاش خیلی معروف اند و بعضی ها گمنام. با کمک هوش مصنوعی تونستند جواب های این سوالات رو با جستجو در ادبیات موجود پیدا کنند(دقت کنید اینجا AI خودش چیزی حل نکرده، مرور ادبیات انجام داده و گزارش داده: این چیزایی که می گید open، قبلا اصلا حل شده)
https://www.erdosproblems.com/339
https://www.erdosproblems.com/1043
https://www.erdosproblems.com/494
https://www.erdosproblems.com/621
https://www.erdosproblems.com/822
https://www.erdosproblems.com/903
می گه اگر از انسان بخوایم این چیزا رو جستجو کنه معمولا درست و درمون گزارشات منفی رو بیان نمی کنه، یعنی اینکه بیاد بگه چیزی پیدا نشد(از ترس اینکه بعدا پیدا بشه و ضایع بشه)
https://mathstodon.xyz/@tao/115385022005130505
می گه نمونه اش literature review هست، وقتی روی یه مساله معروف کار می کنی، مرور ادبیات سخت نیست، خود پژوهشگر می تونه کارو پیش ببره، ولی وقتی مساله منابع کم و یا پراکنده ای داره، پیدا کردن منابع سخت و طاقت فرسا است.
یه مثال می زنه در مورد سایت
https://www.erdosproblems.com/
می گه بالای هزارتا مساله از اردوش توش هست که حدود ۶۰۰ تا حل نشده است، بعضی هاش خیلی معروف اند و بعضی ها گمنام. با کمک هوش مصنوعی تونستند جواب های این سوالات رو با جستجو در ادبیات موجود پیدا کنند(دقت کنید اینجا AI خودش چیزی حل نکرده، مرور ادبیات انجام داده و گزارش داده: این چیزایی که می گید open، قبلا اصلا حل شده)
https://www.erdosproblems.com/339
https://www.erdosproblems.com/1043
https://www.erdosproblems.com/494
https://www.erdosproblems.com/621
https://www.erdosproblems.com/822
https://www.erdosproblems.com/903
می گه اگر از انسان بخوایم این چیزا رو جستجو کنه معمولا درست و درمون گزارشات منفی رو بیان نمی کنه، یعنی اینکه بیاد بگه چیزی پیدا نشد(از ترس اینکه بعدا پیدا بشه و ضایع بشه)
https://mathstodon.xyz/@tao/115385022005130505
Mathstodon
Terence Tao (@tao@mathstodon.xyz)
I am increasingly of the opinion that the most productive near-term adoptions of AI in mathematics will primarily come not from applying the most powerful models to the most challenging problems (although we will see a few isolated examples of progress along…
❤17👏11
Mathematical Musings
این واژه ها توی اثبات و استدلال استفاده می شند و انتخاب هر کدوم موضع نویسنده رو نشون می ده: ۱.دقیق و رسمی، ۲.بی طرفانه و ۳.مبهم و حتی مغرضانه!
معروفه که توی یه مقاله ای نویسنده وقتی داشته یه سری انتگرال رو محاسبه می کرده، می نویسه: انتگرال های قهرمانانه یا طاقت فرسا یا همچین چیزی. اشاره به سختی محاسباتی که داشته انجام می داده(اصطلاحی که به کار بردنش خیلی هم معمول نیست در مقالات)
چند سال بعد که داشته به همون انتگرال ها ارجاع می داده و ازشون استفاده می کرده می نویسه: "می بینیم که" یا "داریم".
چند سال بعد که داشته به همون انتگرال ها ارجاع می داده و ازشون استفاده می کرده می نویسه: "می بینیم که" یا "داریم".
✍15❤2
مرگ یک توپولوژیست
ظاهرا آقای
Andrew Casson
دار فانی رو وداع گفته. زمینه کاری اش
geometric topology
بود، هیچ وقت رساله دکتراش رو تموم نکرد.
در زمینه
high-dimensional
منیفلدها و همین طور منیفلدهای ۳ و ۴ بعدی کار کرده بود. کارهاش نقش اساسی در اثبات حدس پوانکاره در بعد ۴ داشت.
یه invariant هم به نامش هست به اسم
Casson invariant.
ظاهرا آقای
Andrew Casson
دار فانی رو وداع گفته. زمینه کاری اش
geometric topology
بود، هیچ وقت رساله دکتراش رو تموم نکرد.
در زمینه
high-dimensional
منیفلدها و همین طور منیفلدهای ۳ و ۴ بعدی کار کرده بود. کارهاش نقش اساسی در اثبات حدس پوانکاره در بعد ۴ داشت.
یه invariant هم به نامش هست به اسم
Casson invariant.
❤33👏3🤔1
به صورت رسمی جایی منتشر نشده البته و عنوانش هم می گه اثبات دقیق ریاضی نیست.
بیشتر شبیه فیلم های علمی تخیلی می مونه، حتی اسم نویسنده ها!
https://fermatslibrary.com/p/4ceb2280
بیشتر شبیه فیلم های علمی تخیلی می مونه، حتی اسم نویسنده ها!
https://fermatslibrary.com/p/4ceb2280
❤10👏3🤣1🆒1
Mathematical Musings
If you drop a map of your country on the floor, there will be a point on the map that touches the actual point it refers to. Brouwer's fixed point theorem .
Every position of Rubik's cube can be solved in at most 20 half-turn moves. Moreover there are positions for which 19 moves is not enough.
🔥16❤4👏3
Forwarded from Science and Religion (M.M.J)
#پیام_موقت
🖤 انّا للّه و انّا الیه راجعون🖤
«بازگشت همه به سوی اوست»
درگذشت تاسفبار استاد گرانقدر، آقای دکتر ناصر بروجردیان را به جامعه دانشگاهی، خصوصا اساتید و دانشجویان دانشکده ریاضی و علوم کامپیوتر دانشگاه صنعتی امیرکبیر تسلیت عرض نموده، و از خداوند متعال، علو درجات برای آن مرحوم و صبر و شکیبایی برای خانواده محترم ایشان مسألت مینماییم.
برای شادی روح آن مرحوم، فاتحهای قرائت بفرمایید.
🖤 انّا للّه و انّا الیه راجعون🖤
«بازگشت همه به سوی اوست»
درگذشت تاسفبار استاد گرانقدر، آقای دکتر ناصر بروجردیان را به جامعه دانشگاهی، خصوصا اساتید و دانشجویان دانشکده ریاضی و علوم کامپیوتر دانشگاه صنعتی امیرکبیر تسلیت عرض نموده، و از خداوند متعال، علو درجات برای آن مرحوم و صبر و شکیبایی برای خانواده محترم ایشان مسألت مینماییم.
برای شادی روح آن مرحوم، فاتحهای قرائت بفرمایید.
❤51✍3🤔2🤣2
یه خواننده آمریکایی توی سال ۱۹۹۴، اسم خودش رو می ذاره: ۵۰ سنت.
حالا این وب سایت گفته اگر بخوایم اثر تورم رو در نظر بگیریم اسمش باید بشه ۱۰۹ سنت!
حالا به زبون دیگه و ساده تر بخوایم بگیم توی سی سال گذشته قیمت ها در آمریکا تقریبا دوبرابر شده، البته دقت کنید که این اتفاق به تدریج افتاده و اگر از اون فرمول معروف که همه مون می دونیم استفاده کنیم، در هر سال قیمت ها ۲.۵ درصد رفته بالا.
این رو دیدم، رفت رو اعصابم، گفتم با شما هم share کنم.
https://50centadjustedforinflation.com/
حالا این وب سایت گفته اگر بخوایم اثر تورم رو در نظر بگیریم اسمش باید بشه ۱۰۹ سنت!
حالا به زبون دیگه و ساده تر بخوایم بگیم توی سی سال گذشته قیمت ها در آمریکا تقریبا دوبرابر شده، البته دقت کنید که این اتفاق به تدریج افتاده و اگر از اون فرمول معروف که همه مون می دونیم استفاده کنیم، در هر سال قیمت ها ۲.۵ درصد رفته بالا.
این رو دیدم، رفت رو اعصابم، گفتم با شما هم share کنم.
https://50centadjustedforinflation.com/
🤣25❤5✍3