بیان مقدمات اثبات قضیه آخر فرما، از نگاه یه دانش آموز سطح بالای دبیرستانی. سعی کرده همه تعاریف رو بیان کنه تا برسه به قضیه. طبیعتا فهمش برای یه دانشجو ریاضی یا... راحت تره.
https://arxiv.org/abs/2508.10362

#دانستنی های_ به درد_نخور ۲۹
می دونستید زمانی که گودل برای گرفتن تابعیت آمریکا برای امتحان مربوط آماده می شد و مجبور شد قانون اساسی آمریکا رو بخونه، متوجه اشکالات منطقی در اون شد و این مساله نگرانش کرده بود؟ ظاهرا انیشتین و... هم برای جلسه مصاحبه تابعیت همراهی اش کرده بود. مصاحبه کننده با اشاره به اتفاقات آلمان نازی بهش گفته بود: حتما با مطالعه قانون اساسی متوجه شدی که اون اتفاقات در آمریکا ممکن نیست بیفته. ظاهرا اطرافیان متقاعدش کردند که نظری درباره تناقضات موجود نده و گودل هم تابعیت آمریکا رو گرفت.

این رو تازه دیدم، ظاهرا مال ۴۰۰۰ سال پیش هست. خیلی علاقه ای به ریاضیات بابلیان و سومریان و بعدش و ... ندارم. با ریاضیات یکی دو قرن اخیر به خصوص قرن بیستم و قرن حاضر این چیزها دیگه شگفت انگیز نیست به نظرم. حالا چی هست اصلا؟ رادیکال دو رو تا چند رقم محاسبه کردند.
1 + 24/60 + 51/60² +10/60³ =1.41421296
(مبنای اعداد ۶۰ بوده اون زمان)
هر جایی هم در موردش مطلب خوندم با تعجب پرسیدند که:
How did they do it?

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 ها گرفتند. حالا چت جی پی تی در حل سوالات توپولوژی مونده بود، این یکی مفاهیم ساده مربوط به دنباله ها رو هم نمی دونه.