[2505.13472] Proof Assistants for Teaching: a Survey
https://arxiv.org/abs/2505.13472
https://arxiv.org/abs/2505.13472
arXiv.org
Proof Assistants for Teaching: a Survey
In parallel to the ever-growing usage of mechanized proofs in diverse areas of mathematics and computer science, proof assistants are used more and more for education. This paper surveys previous...
❤4
Forwarded from Infinity (Hassan Maleki)
شگفتی در دنیای ریاضیات: دختری ۱۷ ساله، حدس ریاضی ۴۰ ساله را باطل کرد!
هانا کایرو (Hannah Cairo)، دانشآموز ۱۷ ساله آمریکایی، موفق شد با ارائه یک مثال نقض هوشمندانه، یکی از حدسهای قدیمی و مهم در حوزه «آنالیز هارمونیک» را رد کند — حدسی که برای مدت ۴ دهه ذهن بهترین ریاضیدانان جهان را به خود مشغول کرده بود.
حدس Mizohata–Takeuchi :
آیا میتوان مجموعههایی با اندازه صفر (از نظر اندازهگیری لبگ) پیدا کرد که در عین حال «مجموعه تعیینکننده» برای توزیعهای متقارن و محدب باشند؟
بهزبان سادهتر: آیا مجموعههای بهظاهر «بیاثر» و «کوچک» میتوانند حاوی تمام اطلاعات یک تابع باشند؟ این مسأله در تقاطع نظریهی اندازه، آنالیز فوریه، و هندسهی محدب مطرح میشود.
هانا موفق شد مثالی بیابد که این فرض را نقض میکند — یعنی مجموعهای با «اندازه صفر» ساخت که برخلاف انتظار، اطلاعات کامل را منتقل نمیکند. این یعنی حدس غلط است!
بسیاری از ریاضیدانان از دقت و خلاقیت استدلال این نوجوان شگفتزده شدهاند.
جالبتر آنکه هانا هنوز دبیرستان را تمام نکرده و امسال وارد دوره دکترا در دانشگاه مریلند خواهد شد!
منبع
@infinitymath
هانا کایرو (Hannah Cairo)، دانشآموز ۱۷ ساله آمریکایی، موفق شد با ارائه یک مثال نقض هوشمندانه، یکی از حدسهای قدیمی و مهم در حوزه «آنالیز هارمونیک» را رد کند — حدسی که برای مدت ۴ دهه ذهن بهترین ریاضیدانان جهان را به خود مشغول کرده بود.
حدس Mizohata–Takeuchi :
آیا میتوان مجموعههایی با اندازه صفر (از نظر اندازهگیری لبگ) پیدا کرد که در عین حال «مجموعه تعیینکننده» برای توزیعهای متقارن و محدب باشند؟
بهزبان سادهتر: آیا مجموعههای بهظاهر «بیاثر» و «کوچک» میتوانند حاوی تمام اطلاعات یک تابع باشند؟ این مسأله در تقاطع نظریهی اندازه، آنالیز فوریه، و هندسهی محدب مطرح میشود.
هانا موفق شد مثالی بیابد که این فرض را نقض میکند — یعنی مجموعهای با «اندازه صفر» ساخت که برخلاف انتظار، اطلاعات کامل را منتقل نمیکند. این یعنی حدس غلط است!
بسیاری از ریاضیدانان از دقت و خلاقیت استدلال این نوجوان شگفتزده شدهاند.
جالبتر آنکه هانا هنوز دبیرستان را تمام نکرده و امسال وارد دوره دکترا در دانشگاه مریلند خواهد شد!
منبع
@infinitymath
🔥51❤8👍2
Infinity
شگفتی در دنیای ریاضیات: دختری ۱۷ ساله، حدس ریاضی ۴۰ ساله را باطل کرد! هانا کایرو (Hannah Cairo)، دانشآموز ۱۷ ساله آمریکایی، موفق شد با ارائه یک مثال نقض هوشمندانه، یکی از حدسهای قدیمی و مهم در حوزه «آنالیز هارمونیک» را رد کند — حدسی که برای مدت ۴ دهه ذهن…
ظاهرا از نوجوانی کتاب های پیچیده ریاضی مطالعه می کرده، در دوران کرونا در دوره های
Math Circle
دانشگاه برکلی شرکت کرده.
ماه ها درگیر حل این مساله بوده و بعد از ارائه مثال نقض کمی در قانع کردن استاد دچار دردسر شده، چون استاد باور نمی کرده که یه حدس چهل ساله رو بتونه حل کنه.
"After months of trying… finally I found a way to construct a counterexample...
It took me a while to convince Ruixiang Zhang… that my proposal was actually correct."
توی مسابقات پاتنام هم در سال ۲۰۲۴ جزء نفرات Top 500 بوده.
Math Circle
دانشگاه برکلی شرکت کرده.
ماه ها درگیر حل این مساله بوده و بعد از ارائه مثال نقض کمی در قانع کردن استاد دچار دردسر شده، چون استاد باور نمی کرده که یه حدس چهل ساله رو بتونه حل کنه.
"After months of trying… finally I found a way to construct a counterexample...
It took me a while to convince Ruixiang Zhang… that my proposal was actually correct."
توی مسابقات پاتنام هم در سال ۲۰۲۴ جزء نفرات Top 500 بوده.
❤27🔥6👏6
Mathematical Musings
ظاهرا از نوجوانی کتاب های پیچیده ریاضی مطالعه می کرده، در دوران کرونا در دوره های Math Circle دانشگاه برکلی شرکت کرده. ماه ها درگیر حل این مساله بوده و بعد از ارائه مثال نقض کمی در قانع کردن استاد دچار دردسر شده، چون استاد باور نمی کرده که یه حدس چهل ساله…
2024.pdf
86.8 KB
سوالات پاتنام سال ۲۰۲۴، برای اینکه مشخص بشه چرا Top 500 داره!
بعضی سوالاتش اینجوریه که فقط صورت سوال رو متوجه می شم...کلا به لحاظ سختی در یک کلاس دیگه است.
بعضی سوالاتش اینجوریه که فقط صورت سوال رو متوجه می شم...کلا به لحاظ سختی در یک کلاس دیگه است.
👍7❤2🫡1
This media is not supported in your browser
VIEW IN TELEGRAM
یه وسیله جذاب که به کمک اون می شه تابع هموگرافیک رو رسم کرد. حتما می دونید که این تابع شکل کلی اش به صورت زیر هست:
f(x)=ax+b/cx+d, c≠0 , ad-bc≠0
یکی از اعضای کانال لطف کردند و این رو فرستادند، ظاهرا زمانی که در دوره دبیرستان بودند همچین وسیله ای رو طراحی کرده بودند.
f(x)=ax+b/cx+d, c≠0 , ad-bc≠0
یکی از اعضای کانال لطف کردند و این رو فرستادند، ظاهرا زمانی که در دوره دبیرستان بودند همچین وسیله ای رو طراحی کرده بودند.
❤18🔥6👎1
اون هندسه ای که در دبیرستان تدریس می شه یه مقطعی در فرانسه می شه گفت به طور کلی از برنامه درسی دبیرستان حذف می شه. حتی شعار مرگ بر هندسه اقلیدسی رو هم می دادند. گروه بورباکی در ایجاد همچین فضایی بی تاثیر نبود، بیشتر تمرکزشون بر تفکر انتزاعی بود. اعتقاد داشتند که اون نوع هندسه بیشتر تمرکزش بر حفظ کردنه و مهارت حل مساله واقعی رو کمتر تقویت می کنه. بیشتر توی زمینه هایی مثل جبر، آنالیز و نظریه مجموعه ها و...کار می کردند.
جایی خونده بودم بعضی از ریاضیدان های برجسته فرانسوی در قرن بیستم اسم بعضی قضیه های معروف هندسه دبیرستانی اصلا به گوششون هم نخورده بود(چون در دوران اون ها تدریس نمی شده) ظاهرا بعدا کم و بیش این نگاه افراطی تغییر کرد و اون رو در برنامه درسی شون قرار دادند.
جایی خونده بودم بعضی از ریاضیدان های برجسته فرانسوی در قرن بیستم اسم بعضی قضیه های معروف هندسه دبیرستانی اصلا به گوششون هم نخورده بود(چون در دوران اون ها تدریس نمی شده) ظاهرا بعدا کم و بیش این نگاه افراطی تغییر کرد و اون رو در برنامه درسی شون قرار دادند.
❤37👍9🤔3👎1
#دانستنی های_ به درد_نخور ۲۷
می دونستید که ماری کوری در سال ۱۹۱۱ و چند سال بعد از مرگ همسرش وارد رابطه ای شد که در زمان خودش یک رسوایی اخلاقی حساب می شد. در اون سال با
Paul Langevin
که یک فیزیک دان و شاگرد پیر کوری وارد رابطه شد. Langevin خودش متاهل بود و گویا با همسرش اختلاف داشت ولی از هم جدا نشده بودند. در سالی که ماری کوری کاندیدای جایزه نوبل بود نامه های عاشقانه این دو نفر در مطبوعات اون زمان در فرانسه درز پیدا کرد. مطبوعات عنوان زنی فاسد و ویرانگر بنیان خانواده رو بهش نسبت دادند.
خودش هیچوقت این موضوع رو انکار نکرد و برخلاف خواست اعضای آکادمی که ازش خواسته بودند در مراسم شرکت نکنه، گفته بود: "زندگی خصوصی من ربطی به کارهای علمی ام نداره."
ظاهرا برای اینکه در امان باشه از حاشیه ها و حملات، مدتی در منزل بورل(ریاضیدان معروف) به همراه فرزندانش زندگی می کرده.
می دونستید که ماری کوری در سال ۱۹۱۱ و چند سال بعد از مرگ همسرش وارد رابطه ای شد که در زمان خودش یک رسوایی اخلاقی حساب می شد. در اون سال با
Paul Langevin
که یک فیزیک دان و شاگرد پیر کوری وارد رابطه شد. Langevin خودش متاهل بود و گویا با همسرش اختلاف داشت ولی از هم جدا نشده بودند. در سالی که ماری کوری کاندیدای جایزه نوبل بود نامه های عاشقانه این دو نفر در مطبوعات اون زمان در فرانسه درز پیدا کرد. مطبوعات عنوان زنی فاسد و ویرانگر بنیان خانواده رو بهش نسبت دادند.
خودش هیچوقت این موضوع رو انکار نکرد و برخلاف خواست اعضای آکادمی که ازش خواسته بودند در مراسم شرکت نکنه، گفته بود: "زندگی خصوصی من ربطی به کارهای علمی ام نداره."
ظاهرا برای اینکه در امان باشه از حاشیه ها و حملات، مدتی در منزل بورل(ریاضیدان معروف) به همراه فرزندانش زندگی می کرده.
❤30👏4🆒3👎2
2403.01010v1.pdf
78.1 KB
جوک های ریاضی معمولا حتی برای دوستداران ریاضی هم منجر به قهقهه نمی شه و بیشتر اینجوریه که فقط متوجه نکته اش می شند.یکی اومده ۶۶ تا جوک ریاضی رو با هم یه جا جمع کرده.
یکی از جوک هاش:
Einstein-Pythagoras equation:
E = m(a²+b²)
یکی از جوک هاش:
Einstein-Pythagoras equation:
E = m(a²+b²)
🤣40✍3👌3❤2🫡2🆒2
دارم یه مقاله می خونم(چون عنوانش مودبانه نیست، نمی تونم اینجا بذارم) درباره اینکه الگوریتم ها هم می تونند بایاس داشته باشند؟ بایاس رو می گه سه نوع می تونه باشه: آماری، شناختی(مثل اون چیزی که برای انسان پیش میاد) و سیاسی(اعمال تبعیض علیه گروهی خاص)
نویسنده می گه خیلی وقت ها این الگوریتم ها هستند که تصمیم می گیرند کی قبول بشه، کی استخدام بشه، کی حذف بشه و... می گه الگوریتم ها در سکوت نابرابری اجتماعی رو بازتولید می کنند بدون اینکه مسئولیتی رو به گردن بگیرند.
مثال های دم دستی اش الگوریتم های پیشنهاددهنده محتوا و موتورهای جستجوی مقالات و سیستم های ارجاع دهی هست.
یه اتفاق معروف که در مقاله هم بهش اشاره می شه این بود که سال ۲۰۲۰ به خاطر کرونا امتحانات پیش دانشگاهی در انگلیس لغو شد و قرار شد براساس یه الگوریتم کامپیوتری نمرات رو تعیین کنند. مشکل این بود که اگر کسی تو مدارس ضعیف تر درس می خوند الگوریتم نمره پایین تری بهش می داد ولی دانش آموزان مدارس خصوصی نمره بالاتری می گرفتند.
ظاهرا خیلی ها توی پذیرش در دانشگاه به مشکل برخوردند و کلی اعتراض هم شد و در نهایت هم کنار گذاشتند اون روش رو.
به هر حال جالب بود.
نویسنده می گه خیلی وقت ها این الگوریتم ها هستند که تصمیم می گیرند کی قبول بشه، کی استخدام بشه، کی حذف بشه و... می گه الگوریتم ها در سکوت نابرابری اجتماعی رو بازتولید می کنند بدون اینکه مسئولیتی رو به گردن بگیرند.
مثال های دم دستی اش الگوریتم های پیشنهاددهنده محتوا و موتورهای جستجوی مقالات و سیستم های ارجاع دهی هست.
یه اتفاق معروف که در مقاله هم بهش اشاره می شه این بود که سال ۲۰۲۰ به خاطر کرونا امتحانات پیش دانشگاهی در انگلیس لغو شد و قرار شد براساس یه الگوریتم کامپیوتری نمرات رو تعیین کنند. مشکل این بود که اگر کسی تو مدارس ضعیف تر درس می خوند الگوریتم نمره پایین تری بهش می داد ولی دانش آموزان مدارس خصوصی نمره بالاتری می گرفتند.
ظاهرا خیلی ها توی پذیرش در دانشگاه به مشکل برخوردند و کلی اعتراض هم شد و در نهایت هم کنار گذاشتند اون روش رو.
به هر حال جالب بود.
🔥22👎3👌2
اومدند تاثیر نوع خاصی از تحریک مغزی به اسم tRNS رو بر یادگیری ریاضیات بررسی کردند و دیدند عملکرد ریاضی در مواردی بهبود پیدا می کنه. ظاهرا افرادی که عملکرد پایین تری داشتند این تحریک بیشترین تاثیر رو روی توانایی ریاضیات در اون ها داشته. ظاهرا اگر در کنار تمرین و یادگیری باشه اثرگذاری اش بیشتر می شه.
https://journals.plos.org/plosbiology/article?id=10.1371%2Fjournal.pbio.3003200&utm_source=chatgpt.com
https://journals.plos.org/plosbiology/article?id=10.1371%2Fjournal.pbio.3003200&utm_source=chatgpt.com
journals.plos.org
Functional connectivity and GABAergic signaling modulate the enhancement effect of neurostimulation on mathematical learning
Different cortical regions have been implicated in mathematical learning, but their causal role is less clear. This study reveals the causal role of the dorsolateral prefrontal cortex and the frontoparietal network in mathematical learning using transcranial…
❤9
Media is too big
VIEW IN TELEGRAM
این تکنیک های جدید ریاضی برای عمل های ساده رو من اصلا منطق پشتش رو درک نمی کنم. این قضیه ظاهرا به کتاب های درسی اینجا هم سرایت کرده. برای یه جمع و تفریق ساده چنان آسمان و ریسمان می بافند که آدم می مونه چی بگه. نمی دونم شاید فلسفه ای پشتش هست و می خواند تفکر الگوریتمی یاد بچه ها بدند یا دلایل دیگری داره. جمعش کن بره پی کارش دیگه.
متن کتاب های درسی(در اینجا ریاضی منظورم هست) در این سال ها همیشه کیفیت پایینی داشته(مخصوصا اون قسمت مقدمه یا ورود به بحث اش)
متن کتاب های درسی(در اینجا ریاضی منظورم هست) در این سال ها همیشه کیفیت پایینی داشته(مخصوصا اون قسمت مقدمه یا ورود به بحث اش)
👍29👎2❤1
ظاهرا FBI برای مدتی به Paul Erdős مظنون می شه و فکر می کرده جاسوسی یا چیزی باشه. حتی یه بار هم به خاطر اینکه وارد یه برج رادیویی می شه دستگیرش می کنند(ظاهرا مشغول فکر کردن به یک مساله ریاضی بوده). البته بعدا متوجه می شند که اردوش خوره ریاضی هست و به چیزی جز ریاضیات فکر نمی کنه:
"Nothing to indicate the subject had any interest in any matters other than mathematics"
https://www.muckrock.com/news/archives/2015/jul/21/nothing-indicate-nothing-indicate-subject-had-any-/
"Nothing to indicate the subject had any interest in any matters other than mathematics"
https://www.muckrock.com/news/archives/2015/jul/21/nothing-indicate-nothing-indicate-subject-had-any-/
🤣22👍6❤3
یه پیشرفت در محاسبه ضرب دو ماتریس. در ده سال گذشته این بهترین بهبود بوده. سه تا پژوهشگر از دانشگاه برکلی تونستند این کار رو انجام بدند. البته ظاهرا این تیپ الگوریتم ها فعلا کاربرد عملی ندارند و بیشتر از جنبه نظری کار اهمیت دارند، چون برای سایزهای معقول و در عمل همون الگوریتم های کلاسیک بهتر عمل می کنه.
https://www.quantamagazine.org/new-breakthrough-brings-matrix-multiplication-closer-to-ideal-20240307/
https://www.quantamagazine.org/new-breakthrough-brings-matrix-multiplication-closer-to-ideal-20240307/
Quanta Magazine
New Breakthrough Brings Matrix Multiplication Closer to Ideal
By eliminating a hidden inefficiency, computer scientists have come up with a new way to multiply large matrices that’s faster than ever.
❤10👏1
Mathematical Musings
یه پیشرفت در محاسبه ضرب دو ماتریس. در ده سال گذشته این بهترین بهبود بوده. سه تا پژوهشگر از دانشگاه برکلی تونستند این کار رو انجام بدند. البته ظاهرا این تیپ الگوریتم ها فعلا کاربرد عملی ندارند و بیشتر از جنبه نظری کار اهمیت دارند، چون برای سایزهای معقول و در…
ضرب معمولی دو ماتریس رو همه می دونند، برای ابعاد بالاتر مثلا یه الگوریتمی که وجود داره الگوریتم
Strassen
هست. میاد به صورت بازگشتی و شکوندن ماتریس به بلوک های کوچکتر ضرب رو محاسبه می کنه.
روی شکل هم مشخص هست که در ابعاد کوچک تر خیلی فرقی نداره در زمان محاسبه و بهتر هست از همون روش معمول استفاده کرد ولی ابعاد که بزرگ تر می شه الگوریتم کارایی خودش رو نشون می ده.
Strassen
هست. میاد به صورت بازگشتی و شکوندن ماتریس به بلوک های کوچکتر ضرب رو محاسبه می کنه.
روی شکل هم مشخص هست که در ابعاد کوچک تر خیلی فرقی نداره در زمان محاسبه و بهتر هست از همون روش معمول استفاده کرد ولی ابعاد که بزرگ تر می شه الگوریتم کارایی خودش رو نشون می ده.
❤12👍5