Every theorem you prove is actually a theorem of Tarski, since it is equivalent to a theorem of Tarski. If you prove that something is in fact independent then it is not a theorem of Tarski, but the proof of its independence is in fact a theorem of Tarski.

با یک روز تاخیر
دیروز تولد خانم
Margaret Hamilton
بود، در ایران شاید تا حدی برای بعضی ها به خاطر مدالی که از اوباما گرفت شناخته شده باشه، به خاطر نقشش در توسعه نرم افزارهای مربوط به پرواز آپولو در سال ۱۹۶۹.
اصطلاح
Software engineering
رو هم ایشون مطرح کرد.
لیسانس ریاضی از دانشگاه میشیگان داره (فقط همین)
ظاهرا اون اوائل می خواسته در زمینه ریاضی محض ادامه تحصیل بده که بعدا مسیرش عوض می شه. غیر از اون پروژه آپولو در پروژه های مختلف دیگه ای هم حضور داشته.
توی یه مصاحبه گفته: در بعضی از پروژه ها به خاطر حساسیت اون ها ما فقط بخشی از کدها که مربوط به یه بخش کوچکی از پروژه بود رو می نوشتیم و هیچ اطلاعی از کل پروژه نداشتیم.
توی عکس هم کنار راهنمای مربوط به محاسبات آپولو وایستاده.

زندگی تارسکی، به قلم سولومون ففرمن منطق‌دان و شاگرد تارسکی، و آنیتا بردمن ففرمن.

همون طور که از اسمش پیداست، آنیتا همسرشه:)

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

مساله برای فکر کردن

یکی از دوستان اشاره کردند این یکی از open problemهای نظریه اعداد هست و به
Andrica's Conjecture
معروفه.
من از اسکرین شات هام برداشتم و حواسم نبود. به هر حال دیگه پاکش نمی کنم.

مساله برای فکر کردن

قدیم یه معادله ساده رو که می خواستند بنویسند نیم صفحه داستان سرایی می کردند. بعد با گذشت زمان و وارد کردن و در واقع نامگذاری برای متغیرها و... اوضاع بهتر شد.
خب الان یه عده می گند این mathایی که ما داریم می خونیم و در واقع می نویسیم زیادی
unformalized
هست. این طرز ریاضی خوندن نیست. آدم های ۲۰۵۰(شایدم زودتر) این کتاب ها و نوشته های ما رو ببیند می گند اینا کی بودند؟
مثلا می گند باید فرض ها رو نامگذاری کنید. مثلا به جای اینکه بگیم:
تابع f(x) مثبت برای x های منفی و y منفیه پس داریم f(y)>0، باید اینجوری بنویسیم:
Hf : for all x < 0, f x > 0
Hy : y < 0
have : f(y) < 0 := Hf Hy
من که موافقم.

من فکر می‌کنم استفاده از زبان صوری، چیزی شبیه به syntactic sugar هست؛ کوتاه‌نویسی که مفهوم رو بهتر می‌رسونه و ردیابیش راحت‌تره.

ولی خب از یه طرف، وقتی تعداد فرض‌های به این شکل زیاد می‌شه، مدیریتشون سخته. اینجا باز هم به روش‌های غیرصوری و تکیه به تجربه باید ببینی کجا کدوم فرض رو خط بزنی که برهانت شلوغ نشه. در پیاده‌سازی کامپیوتری برای شلوغ نشدن باید در موقعیت مناسب مجموعه فرض‌های هر مرحله رو prune کنی، و برای جلوگیری از تکرار کد (مثلا اثبات obligation)، باید بشینی حتما تاکتیک مناسب بنویسی که گاهی خوندن و‌ فهمیدن بعضی از این تاکتیک‌ها از فهمیدن اثبات‌های خوارزمی هم سخت‌تره :")

در کل نام‌گذاری و دسته‌بندی فرض‌ها کار خیلی خوبیه (مخصوصا اونایی که زیاد بهشون در طی اثبات ارجاع داده می‌شه). ولی دیگه اون عده که به ریاضیات الان می‌گن غیرفرمال و غایت آمالشون برهان‌نویسی به سبک

Interactive Theorem Prover

هست، رفتارشون فناتیکه. در بعضی موارد (جلوگیری از تکرار فرض‌ها در هر مرحله، نکات تجربی در اثبات‌کردن که باعث پدید اومدن برهان‌های خوب می‌شه)، صوری نویسی نمی‌تونه جای زبان طبیعی رو بگیره. به علاوه، صوری سازی بیش از حد، دایره‌ی ترمینولوژی رو خیلی بزرگ می‌کنه، چرا که باید هر چیزی دقیق تعریف بشه (و در کیس کامپیوتر تایپ‌چک هم بشه)؛ هر کسی به سبک خودش فرض‌ها رو نام‌گذاری می‌کنه و این طوری وقت زیادی سر فهم ترمینولوژی به کار رفته تو برهان تلف می‌شه، در حدی که آدم می‌تونه از کار اصلیش باز بمونه.

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

موتسارت ریاضیات سعی کرد از سیاست فاصله بگیره ولی سیاست ولش نکرد.
یادداشت اعتراضی تائو به اتفاقات اخیر آمریکا
می گه سیاست مدارها با تصمیمات ناگهانی هنجارهای دیرپای علمی رو نادیده گرفتند.
می گه من در استرالیا بزرگ شدم اما در فضای فرهنگی و علمی آمریکا غوطه ور بودم.
می گه با Sesame Street شمردن یاد گرفتم. می گه آمریکا عشق من به ریاضیات رو عمیق تر کرد. می گه ۲۵ ساله اینجام.
می گه پژوهش های من منجر شده به توسعه الگوریتم هایی که زمان MRI رو خیلی کم کرده. می گه در آمریکا که مهد علم هست و علم در اون یه خیر عمومی هست این وضع رو ایجاد کردند. می گه به خاطر وجود یه کلمه در یه پروپوزال همه چیز رو تعطیل کردند. می گه همیشه از سیاست فاصله گرفتم ولی الان به چیزی حمله شده که بنای زندگی حرفه ایش هست.
https://newsletter.ofthebrave.org/p/im-an-award-winning-mathematician

اینو دیدم یاد صحبتای ششمانی درباره richard thomas افتادم. می گفت یه سری یه چیزی بهش تحویل داده بعد thomas بهش گفته خیلی hand-wayعه و اصلا خوشش نیومده، گویا simplicity و rigor براش خیلی مهمه. یه مصاحبه هم داره که یه خانوم ریاضی دانی این مصاحبه رو ترتیب داده و یه پیج یوتیوب داره که تقریبا مشابه دکتر اصغری با ریاضی دان ها(البته بیشتر تو هندسه جبری) مصاحبه می کنه. لینکش:
https://www.youtube.com/channel/UCYRR0SgbYH59htIHkwTbqMw

ظاهرا در موارد مختلف سوتی از AI ها گرفتند. حالا چت جی پی تی در حل سوالات توپولوژی مونده بود، این یکی مفاهیم ساده مربوط به دنباله ها رو هم نمی دونه.

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

توی سال های اخیر به کمک کامپیوتر تونستند آخر بازی های مختلف رو که معمولا منتهی می شه به چند مهره خاص بررسی کنند. مثلا حالت هایی که حداکثر ۷ مهره در صفحه بازی هست. یعنی طوری شده که مثل یه جدول راهنمای خیلی بزرگ ما تقریبا همه آخر بازی ها رو می دونیم تهش چی می شه. این باعث شد که خیلی از وضعیت هایی که فکر می کردند برد باشه یا باخت با کمک کامپیوتر دیدند نتیجه اش جور دیگه ای شده. بعضی از این وضعیت ها چنان پیچیده و عمیق هستند که هیچ انسانی توانایی تحلیل و بررسی اون رو نداره.

وضعیت بالا معروف ترین حالت برای این مورد هست. سفید بعد از ۵۴۹ حرکت می تونه سیاه رو مات کنه(با فرض اینکه هر دو طرف بهترین حرکت هاشون رو انجام بدند و اینکه محدودیتی برای تعداد حرکات نباشه).

شاید بهتر باشه این مقایسه انسان یا کامپیوتر رو خیلی ادامه ندیم.
خلاقیت، الهام و زیبایی سهم انسان، کامل بودن و محاسبات بی نقص سهم کامپیوتر

حال داشتین بازی رو اینجا دنبال کنید:
https://lichess.org/study/bFo2OOVC/XiCxKfO3

(توجه: این کد رو من ننوشته‌م.)

یه نمونه از همین مدل تاکتیک‌ها در Coq که برای استفاده در اثبات «شکستن یه sequent، وزنش رو کم می‌کنه» هست (اونم به شکل غیرمستقیم و در دل یک تاکتیک مرتبط دیگه که تازه بعدش بری عبارت تو گیومه رو بیان و اثبات کنی). خود قضایایی که بعد از apply نوشته شدن هم بیان و اثبات جدا دارن. حالا شما حساب کن با فرض داشتن تسلط نسبی به Coq و کتاب‌خانه‌ی stdpp (یه پروژه بزرگ در موسسه ماکس پلانک که توش ساختارهای ریاضی که زیاد استفاده می‌شن رو با قضایای مربوط بهشون پیاده‌ کرده‌ن، که دیگه کسی وقتش رو سر پیاده‌سازی اینا تلف نکنه و کار اصلیش رو انجام بده)، چه قدر وقت باید بذاری ببینی عبارات سبز رنگ چی‌ئن یا اصلا چرا تو عین این کد رو برای پروژه خودت می‌زنی، چرا تایپینگ ضمنی برای این داره کار می‌کنه ولی برای تو نه.

مساله برای فکر کردن

حتی پاکستان هم نسخه مخصوص به خودش رو داره.
معمولا ممکنه کیفیت چاپ کمی پایین باشه، ولی خب قیمتش هم خیلی پایین تره.

این بحث جالبیه، جدا از فان بودنش بعضی وقت ها نکات آموزشی جالبی هم داره. در این لینک Mathoverflow فهرستی از این مسائل رو لیست کردند.
اینقدر تنوع داره مثال هاش که قطعا یه مورد جالب توجه توی اون ها پیدا می کنید.
https://mathoverflow.net/questions/42512/awfully-sophisticated-proof-for-simple-facts