TGViewer
Channel Public Channel
a pessimistic researcher

a pessimistic researcher

@apessimisticresearcher

جهان ما از دیتابیس و فرمال متد شروع میشه و به پوچی ختم میشه!
Subscribers
2.38K
Photos
764
Videos
95
Links
1K
Recent Posts 20 shown
Post #5553 524
از اونجایی که ما جلسه آنلاین و پرسش و پاسخ نخواهیم داشت، حوصله گروه و این داستان‌ها هم نیست، همیشه می‌تونید قبل و بعد هر جلسه هر سوالی داشتید برام بفرستید که توی ویدیو‌ها پاسخ بدم براتون. مثلا اگر چیزی از کتاب و یا مباحثی که قراره باهاشون مواجه بشیم هست که دوست دارید در موردشون صحبت بشه و یا کلا سوالیه که به نظرتون خوبه در این دوره بهش پرداخته بشه رو برام بفرستید و من سعی می‌کنم توی ویدیوها بهشون پاسخ بدم (سوال در حد اینکه Verification چیه یا سوالات کلی این شکلی رو مطمئن باشید توی ویدیوها توضیح میدم).
محتویات شامل اسلاید‌ها، نوت‌ها، تمارین، پروژه‌ها و فرمال‌سازی مباحث کتاب در LEAN رو توی این ریپازیتوری قرار میدم:
https://github.com/joulook/winskel
GitHub GitHub - joulook/winskel Contribute to joulook/winskel development by creating an account on GitHub.
Post #5552 553
Debrary The Formal Semantics of Programming Languages: An Introduction - Glynn Winskel - The MIT Press - 1993 @debrary
بر اساس این کتاب دارم یک سری ویدوی ضبط میکنم که به نظرم شروع خوبی برای ورود به دنیای PL و Verification هستش. و قصد دارم توی ویدیو اول بهتون بگم که چرا باید امروز کتابی که سال ۱۹۹۳ چاپ شده رو خوند.
Post #5547 1.33K
a pessimistic researcher آقای Richard S. Sutton برنده‌ی جایزه تورینگ، یه مقاله‌ای داره به اسم The Bitter Lesson که اگر اشتباه نکنم سال ۲۰۱۹ منتشرش کرد (دوره‌ای که هیچ اثری از LLM ها نبود و اون دوران بلاک‌چین و ML و Data Science حسابی روی هایپ بودن). من این مقاله رو اولین بار پارسال…
The sweeter lessson
Post #5546 1.4K
تک درختم سوخت
سیکیم جنگل صاحابی
Post #5545 1.36K
a pessimistic researcher آقا تا ۱۳ نوامبر ترو خدا دیگه چیزی حل نکنید ما این مقاله مون رو فرو کنیم تو PLDI بعدش هر گهی میخواید بخورید، بخورید. به تخمم میرم کشاورزی.
دیدید ترسم بی‌جا نبود؟
آقای Jukka Suomela توی لینکدین امشب پست گذاشته:
I think our research community should seriously start to have this conversation:

How do we plan ahead for the day OpenAI releases their next-generation model?

That day, dozens of students, postdocs and professors all around the world will feed the same standard open questions to the model. Say, in our case, questions like "what is the exact complexity of distributed (Δ+1)-coloring in the LOCAL model?" They all burn their tokens and all of them get a solution, essentially the same solution. Then what? All of them rush to understand the solution, write it up nicely, and try to be the first to submit somewhere? And the incentives are set so that the one who dares to submit half-baked slop first wins, and dozens of smart people wasted their time and effort?

How could we plan ahead so that the end result is not just tons of wasted effort, time, and money, with huge amounts of redundant uncoordinated parallel work?
Post #5544 1.5K
دلم اون دورانی رو میخواد که کدکس برند کاندوم بود و نه چیز بیشتر
Post #5543 1.17K
شب‌ها به کنج codex ام آواز می‌دهند
کای Astra گنج فرمالیان باز می‌دهند
Post #5542 1.24K
a pessimistic researcher "The Bitter Lesson of Being Brainiac in the era of Speed Demons" Part I —————————————— پرده‌ی اول (آفرینش) : تصور کنید یک دستگاه تایپ داریم که یک میمون پشت این دستگاه نشسته. اگر این میمون شروع کنه به طور رندوم کلیدهای این دستگاه تایپ رو فشار بده، با اختصاص…
آقای Richard S. Sutton برنده‌ی جایزه تورینگ، یه مقاله‌ای داره به اسم The Bitter Lesson که اگر اشتباه نکنم سال ۲۰۱۹ منتشرش کرد (دوره‌ای که هیچ اثری از LLM ها نبود و اون دوران بلاک‌چین و ML و Data Science حسابی روی هایپ بودن). من این مقاله رو اولین بار پارسال سر کلاس استادم خوندم و تا اون موقع از وجودش با خبر نبودم. داستان مقاله به طور خلاصه اینه که تاریخ یه درسی به ما داده و اون درس اینه که : روش‌های general که متکی بر توان محاسباتی هستند همواره نسبت به روش‌های مبتکرانه‌ای که نشأت گرفته از هوش و دانش انسانی هستند، موثرترند و میتونن Scale-up بشن. این قضیه تو حوزه معماری کامپیوتر رخ داد مثلا تقابل RISC و CISC که در آخر RISC تنها با تکیه بر این ایده ساده که به جای خلق مدارهای پیچیده و هوشمند، بیا مدارهای ساده رو چند برابر و سریع‌تر کن پیروز شد. این قضیه توی شطرنج رخ داد، توی Vision رخ داد، توی AI رخ داد، توی NLP رخ داد و حتی به نظرم توی Software Analysis هم رخ داد. یعنی توی تمام این حوزه‌ها effort اولیه این بود که بیایم با استفاده از دانش و تجربه‌ی انسانی الگوریتم‌های پیچیده و مبتکرانه‌ای ارائه بدیم، و بعد از مدتی که دیدیم نخیر این سقف شیشه‌ای از بالای سرمون تکون نمیخوره، با شیطان پیمان ببندیم و به جای اینکار روش‌های فوق‌العاده ساده و naive رو اتخاذ کنیم ولی سعی کنیم با افزایش توان محاسباتی، برنده این بازی بشیم. و شدیم.

یه چیزی که برام خیلی جالبه اسم این درسه، Bitter. چرا این درس تلخه؟ خود نویسنده معتقده تلخی این درس بدین خاطر هست که انسان همواره از نظر روانی، کار و تلاش ذهنی و فکری براش یک ارزش والا و معنوی به خصوصی داره که با کمتر چیزی در دنیا میتونه مقایسه‌اش کنه. وقتی این ارزش بخواد به چالش کشیده بشه، قطعا خشم و عصیان فراوانی رو به همراه خودش داره. اون زمان که این مقاله رو میخوندم شاید هم خودم هم استاد و شاید حتی همین الان خیلی‌ها معتقد بودیم و هستند که درس‌های Sweet هم وجود داره. مثلا Automated Reasoning. حتی آقای Moshe Vardi یکی دو ماه پیش یه مقاله نوشت به اسم The Sweeter Lesson و اونجا گفت که مقاله‌ی آقای ریچارد خیلی بدبینانه است و تجربه‌ی SAT و SMT به ما نشون میده که درسای شیرینی هم هستند. منتهی به نظرم آقای Vardi خیلی خوب در جریان تحولات و تغییرات همون کامیونیتی نبود. توی این پست نوشتم در موردش، منتهی خود ایشونم به نظر میاد که توقع دیدن این همه پیشرفت رو نداشت چرا که پست‌های اخیرشون توی لینکدین بیشتر تم وحشت و تحیر داره.

خلاصه چیزی که هست اینه که این درس تلخ در تمام جبهه‌های علم داره به پیروزی میرسه و حق میدم اگر کسی نتونه در زمان کوتاه و به راحتی بپذیردش. بعد روانی مسئله‌ خیلی سهمگینه. ولی به نظرم چند ماه دیگه، همگی با این قضیه کنار اومدیم و با تلخی این درس دوست میشیم.

به بهانه‌ی این حرفا من سال گذشته یه پستی نوشتم با عنوان The Bitter Lesson of Being Brainiac in the era of Speed Demons که سه قسمته. اگر حوصله داشتید بخونید ولی حواستون باشه که اون موقع من خیلی موافق این درس تلخ نبودم. واسه همین یه جاهاییش نیاز به رقیق سازی داره.
Post #5541 1.06K
آقا تا ۱۳ نوامبر ترو خدا دیگه چیزی حل نکنید ما این مقاله مون رو فرو کنیم تو PLDI بعدش هر گهی میخواید بخورید، بخورید.
به تخمم میرم کشاورزی.
Post #5540 1.1K
From Diomidis Spinellis blog : Thinking will become a hobby

These lines are very difficult for me to write because I feel like digging my own grave. AI systems are improving by leaps and bounds. From the early 2022 fumbling release of ChatGPT, which couldn’t correctly count the number of a’s in my name (it claimed two), we reached OpenAI’s release of math papers where an internal AI model solved many hundreds of previously open math problems. Aside from philosophical arguments, practical claims regarding the superiority of human thought, on grounds such as hallucinations or bias, increasingly appear to me like rearguard defence. For the bulk of today’s cognitive work, the writing’s on the wall: AI will take over.

The three factors driving AI’s dominance in the modern work environment are better performance, lower cost, and higher availability. The performance of AI models is rising spectacularly on all fronts: perception, knowledge processing and creation, reasoning, judgement, and autonomous action. In parallel, human proficiency in key information-processing skills, low on average among adults, is even declining among students. Consequently, AI systems are performing better than humans in ever-wider range of tasks.

AI’s cost is also falling due to huge investments and scientific progress. Successive generations of AI models offer superior performance at lower cost, with older models retained only for backward compatibility. As a result, it is making financial sense to replace or augment human labour with AI systems across an increasingly broad range of activities.

Finally, and most obviously, AI systems can operate around the clock, without the need for rest or breaks. They can also help alleviate labour shortages arising from demographic trends or skills gaps. Meanwhile, trillions of dollars in projected data centre investment through 2030 are set to bring vast additional AI processing capacity online.

As happened in past technological revolutions, there will undoubtedly be fierce resistance to the replacement of cognitive work with AI. This time it will be fiercer because, unlike previous revolutions, which transformed manual labour, AI challenges knowledge workers, whose specialised expertise, control over information, and decision-making authority afford them greater economic and organisational power. Governments will try to clip AI’s wings through regulation and taxation. Such actions didn’t quell past revolutions so there’s little reason to believe they’ll work now.

So what’s the fate of human thought? My take is that cognitive work will diminish. Thought will increasingly become a leisure pursuit, as hunting did following animal domestication, calligraphy after typography, woodworking after industrialisation, and horse riding after motorisation. Machines transformed much of physical activity from necessity into choice; similarly, AI will decouple human thinking from its economic purpose.

I’ll end with my thoughts on how to prepare for and live through this transition. My take is that building this AI-driven world, riding through the bumps along the road, and preparing to live a fulfilling and satisfying life in an environment where AI dominates cognitive work will be hugely demanding, stressful, and intellectually challenging. Such is the nature of revolutions. Consequently, we must keep pace with and capitalise on AI’s advances; be flexible, adaptable, and resilient; and build a purposeful and rewarding life beyond work. My challenge ahead is to move from making a living by thinking, to making thinking part of a life worth living.
Post #5539 1.07K
شما میتونید ۵ مرحله سوگواری رو از روی ری‌اکشن‌های دو پست آخر ببینید
۱. انکار اونایی که دیسلایک کردن
۲. خشم اونایی که فاک و پوپ دادن
۳. چانه زنی، اونایی که کامنت میذارن و توجیه میکنن
۴. افسردگی اونایی که گریه گذاشتن
۵. پذیرش اونایی که 🥰 گذاشتن
Post #5537 1.29K
فاک فاک فاک
این مقاله و ریزالتی که داده کل Algorithms Design و Fine-grained complexity رو متحول میکنه.

نکته جالبش این قسمته :)

How the result was originally found and shared with the authors. An Anthropic employee used an internal research model to investigate open problems in the theory of cryptography. One of them was about cryptographic constructions based on the average-case hardness of Zero-k-Clique [LLV19, AHY25]. Claude was tasked with verifying and improving the constructions, but instead developed this algorithm, first for the average case, then for the worst case. The session used 16M output tokens with no human input. Anthropic shared the algorithm with the authors in September 2026 under a confidentiality agreement, offered compensation, and provided access to the public version of Claude.

یعنی کلا این داستان بدون دخالت انسان صورت گرفته و فقط برای اینکه مطمئن بشن هیچ خطایی نیست دادنش این دوتا بخونن و بفهمنش و تفسیرش کنن. بعد یارو نشسته هنوز داره توی کانالش مینویسه میگن که AI دشمن فلان نیست و خاله‌ی فلانه و این حرفا. بخدا همه چیز تموم شده. تمام شد!
کاملا تمام شد!
هیچ وقت اینقدر تمام نشده بود!
نمیتوانید باور کنید تا چه حد تمام شده است!
Post #5535 1.27K
a pessimistic researcher یادمه آقای Dana Scott توی یکی از مصاحبه‌هاشون میگفن که Alfred Tarski که استاد راهنماشون در مقاطع پیش از دکتری بودن به قدری سیگار می‌کشید بین حرفاش که ما همیشه سر کلاس‌هاش این ترس رو داشتیم که الان با سیگار روی تخته می‌نویسه و گچ رو اسموک میکنه :)
تارسکی 🚬
Post #5534 1.1K
هر وقت لای اثبات یه چیز توی تایپ‌تئوری و لاجیک رو باز میکنی، مثل این اثبات پای یه کسشری از آقای Tarski در میونه. تو کی بودی مرد.
Post #5533 1.11K
a pessimistic researcher دروغ چرا از صبح نشستم پای این مث openAI و دارم سعی می‌کنم یکم درک کنم که چه اتفاقی افتاده. یکی از مسائلی که این بابا حل کرده Weak and strong normalization in pure type systems هستش. این مسئله رو اولین بار آقای Jan Herman Geuvers تحت عنوان یک Conjecture توی…
اگر اشتباه نکنم توی یکی از جلسات حلقه‌ی مطالعاتی Programming Languages & Logic که پارسال با همت دوستان کانال پیش بردیم، این حدس رو بحث کردیم در موردش.
Post #5532 1.08K
دروغ چرا از صبح نشستم پای این مث openAI و دارم سعی می‌کنم یکم درک کنم که چه اتفاقی افتاده. یکی از مسائلی که این بابا حل کرده Weak and strong normalization in pure type systems هستش. این مسئله رو اولین بار آقای Jan Herman Geuvers تحت عنوان یک Conjecture توی تز دکتری‌شون سال ۱۹۹۳ عنوان کردن. ۸۰ صفحه اثباته. دیوانه کننده است.
GitHub math/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf at main · openai/math Contribute to openai/math development by creating an account on GitHub.
Post #5531 994
مپش قوی بود ایشالا وار بعدی
Older posts →

About this channel

How can I read @apessimisticresearcher without a Telegram account?
TGViewer shows the public web preview Telegram publishes for a pessimistic researcher: recent posts, photos, videos and the subscriber count, with no app, login or account.
How many subscribers does a pessimistic researcher have?
a pessimistic researcher (@apessimisticresearcher) has 2.38K subscribers on Telegram, refreshed roughly every 30 minutes.
Does a pessimistic researcher know I viewed it here?
No. Public channel previews carry no viewer identity, and TGViewer has no accounts or tracking of what you look up.
Threads Profile ViewerView any public Threads profile without an account.Open ThreadLook →Writing with AI? Make it sound human.Metric37 rewrites AI drafts so they read naturally. Free AI detector, 1,500 words free.Try Metric37 →