کورت گودل، منطق‌دان اتریشی، یکی از خلاقانه‌ترین متفکران قرن بیستم بود. دو قضیه ناقصیت او که در سال ۱۹۳۱ منتشر شد، ریاضیات را متحول کرد و راه را برای عصر دیجیتال هموار ساخت.
پس از نتایج بنیادین گودل در دهه ۱۹۳۰، او تنها چند مقاله محدود منتشر کرد. با این حال، آثار منتشرنشده او به ده‌ها هزار صفحه می‌رسد و برای مورخان علم بسیار جذاب است.
از سال ۲۰۱۷، یان فون پلاتو، منطق‌دان فنلاندی، پروژه‌ای را در دانشگاه هلسینکی برای درک محتوای ۱۶ دفترچه‌ای که گودل در اوایل دهه ۱۹۴۰ نوشته بود، هدایت کرده است. این مواد موسوم به «دفترچه‌های کاری»، شامل ۱,۰۰۹ صفحه متن فشرده درباره ریاضیات و منطق است. بخش عمده‌ای از آن به سبک اختصاری آلمانی گابلزبرگر (Gabelsberger) نوشته شده که حتی زمانی که گودل از آن استفاده می‌کرد نیز منسوخ محسوب می‌شد.
پیشرفت در فهم ریاضی متن به‌طرز دردناکی کند بود – حدوداً هفته‌ای یک صفحه – تا اینکه در ماه سپتامبر، فون پلاتو کمک مدل هوش مصنوعی کلود را به خدمت گرفت. ظرف چند روز، کلود خلاصه‌ای جامع از کل مواد ارائه کرد که نشان داد گودل صدها قضیه‌ای را اثبات کرده است که هیچ‌کس از وجود آن‌ها خبر نداشت.
معروف‌ترین منطق‌دان دوران مدرن، در واقع، چیزهای مهم‌تری نسبت به آنچه تصور می‌شد کشف کرده بود.
«من کاملاً حیرت‌زده شدم،» گفت فون پلاتو. «این دفترچه‌ها نه تنها ده‌ها پیش‌بینی از نتایجی را دارند که تا دهه‌های ۷۰ و ۸۰ میلادی ناشناخته بودند، بلکه شامل ۱۴ موضوع در منطق نیز می‌شوند که هیچ‌گاه پیگیری نشده‌اند. گودل بسیار فراتر از زمان خود بود.»
گودل مسیر منطق را تغییر داد زیرا مرزهای دانش ریاضی را آشکار ساخت. قضایای ناقصیت او نشان می‌دهند که در تمام سیستم‌های ریاضی، گزاره‌های حقیقی وجود دارند که نه می‌توان آن‌ها را اثبات کرد و نه رد نمود. اگرچه این نتیجه ضربه‌ای به نسل‌های قبلی منطق‌دانان بود که امیدوار بودند همه حقایق قابل راستی‌آزمایی باشند، اما آثار گودل این حوزه را به سمت‌های جدیدی سوق داد و الهام‌بخش آلن تورینگ برای نوشتن مقاله سال ۱۹۳۶ خود شد که نظریه محاسبات مدرن را آغاز کرد.
در سال ۱۹۴۰، گودل از اتریشِ تحت حکومت نازی‌ها گریخت. او در پرینستون، نیوجرسی ساکن شد و در مؤسسه مطالعات پیشرفته (Institute for Advanced Study) دوست صمیمی آلبرت انیشتین گردید. در سال‌های پایانی عمر، دچار پارانویای شدید شد و از خوردن غذاهایی که توسط همسرش طبخ نشده بودند امتناع ورزید و سرانجام در سال ۱۹۷۸ بر اثر قحطی جان سپرد.
فون پلاتو گفت که پروژه گودل خود را در سال ۲۰۱۷ آغاز کرد زیرا با بازنشستگی اجباری از دانشگاه هلسینکی مواجه بود. «کاری کنم که غیرقابل جایگزین شوم؟ آره، شروع به خواندن صفحات مرموز و اختصاری گودل می‌کنم!» او گرنتی معادل ۲.۵ میلیون یورو (۲.۱ میلیون پوند) از شورای تحقیقات اروپا دریافت کرد، سبک اختصاری گابلزبرگر را به صورت خودآموز فرا گرفت – «من یکی از تنها شش نفر در جهان هستم که می‌توانم آن را بخوانم» – و تیم کوچکی تشکیل داد.
در ماه آگوست، در کنفرانسی در فرانسه درباره هوش مصنوعی و اثبات قضایا، فون پلاتو با دانشمندان علوم رایانه‌ای دیدار کرد که پیشنهاد کردند از کمک کلود برای فهمیدن دفترچه‌های کاری بهره ببرد. پس از بازگشت به هلسینکی، او این فرآیند را آغاز کرد و رونوشت‌های خود از دفترچه‌ها را به همراه شش کتابی که قبلاً درباره گودل و سایر ادبیات علمی ثانویه نوشته بود، در اختیار کلود قرار داد.
«ظرف چند روز، توضیحی ۶۵۰ صفحه‌ای از دفترچه‌های کاری را دیدم. باید صفحه به صفحه کنترل می‌شد، اما اساساً کاری است که انجام آن برای انسان‌ها غیرممکن است،» او گفت. «انسان‌ها صفحه به صفحه می‌خوانند و معمولاً چیزها را فراموش می‌کنند. ما حدود یک سال طول می‌کشیم تا حدود ۵۰ صفحه را بخوانیم. ما صرفاً قادر نیستیم تمام بخش‌های مختلف را در ذهن نگه داریم.
«هوش مصنوعی می‌تواند تمام قطعات را در هزار صفحه به هم متصل کند. او می‌تواند تمام نوشته‌های گودل را به عنوان یک کل واحد ببیند.»
قضایای ناقصیت گودل وجود گزاره‌هایی را آشکار کرد که حقیقت آن‌ها مستقل از سیستمی است که در آن نوشته شده‌اند؛ یعنی نمی‌توان آن‌ها را در چارچوب آن سیستم اثبات یا رد کرد. در سال ۱۹۶۶، پل کوهن، ریاضیدان آمریکایی، برای نشان دادن استقلال دو گزاره معروف ریاضی – فرضیه پیوستگی و بدیهی انتخاب – مدال فیلدز، بالاترین افتخار در ریاضیات، را کسب کرد.
گودل در واکنش به مدال فیلدز کوهن گفت که او همین نتیجه را در دهه ۱۹۴۰ اثبات کرده بود. اما وقتی همکارانش اصرار کردند که اثباتی ارائه دهد، گودل نتوانست آن را از یادداشت‌های خود بازسازی کند.
اولین تکلیفی که فون پلاتو به کلود داد، کشف این بود که آیا دفترچه‌های کاری گودل اثباتی برای استقلال بدیهی انتخاب دارند یا خیر؛ چیزی که نشان می‌داد گودل در سال ۱۹۶۶ راست گفته است. پاسخ آمد: بله، تقریباً. «او فقط یک قدم فاصله داشت،» گفت فون پلاتو. «تعریفی وجود دارد که گودل اشتباه نوشته است، اما دو سال قبل تعریف درست را داشته است، بنابراین این ایده مطرح است که اگر فقط چند ماه دیگر ادامه داده بود، به همان تعریف درست می‌رسید. برای من، معماری اثبات او فوق‌العاده زیباست. او تمام این نتایج نظریه مجموعه‌ها را الگویی یکنواخت دنبال می‌کند.
«آنچه بیش از همه توجه مرا جلب می‌کند این است که او از ایده‌ها شروع می‌کند. او مانند کسی نیست که با فرمول‌ها بازی کند و امیدوار باشد به جایی برسد. او ایده‌های بسیار، بسیار روشنی دارد و سپس نظام‌مند عمل می‌کند. قدم به قدم پیش می‌رود و موفق می‌شود اهداف خود را در این کار رسمی محقق سازد.»
فون پلاتو گفت که وقتی کلود اثبات بازسازی‌شده استقلال بدیهی انتخاب را به او ارائه داد، او آن را از طریق دستیار اثبات Coq – برنامه‌ای که اعتبار اثبات‌های ریاضی را بررسی می‌کند – اجرا کرد و قبول شد. فون پلاتو معتقد است اگر گودل آثار خود را درباره بدیهی انتخاب منتشر می‌کرد، مدال فیلدز سال ۱۹۴۰ را می‌برد. «شاید او احساس می‌کرد وقتی کوهن مدال را گرفت، چیزی را از دست داده است.»
در مکالمات بعدی با کلود، فون پلاتو از مدل هوش مصنوعی خواست تمام قضایای موجود در دفترچه‌ها را استخراج کند که گودل برای آن‌ها اثبات کامل، طرح اولیه اثبات یا ایده‌ای برای اثبات داشت. کلود ۶۶۳ مورد یافت. وقتی این نتایج وارد Coq شدند: «حدود ۴۰۰ مورد دقیقاً همانطور که بیان شده بودند تأیید شدند، حدود ۲۰۰ مورد اصلاح شدند، به این معنا که شاید بیان قضیه باید دقیق‌تر می‌شد یا فرضی اضافه می‌گردید. حدود ۵۰ مورد غلط بودند و این جای تعجب ندارد. خود گودل هنگام مرور دوباره یادداشت‌هایش، گاهی حاشیه‌نویسی می‌کرد: falsch! [غلط] یا schlecht! [بد].»
فون پلاتو افزود: «من مطمئنم که مطالعه مداوم دست‌نوشته‌های گودل گنجینه‌های بیشتری را آشکار خواهد کرد. طبق گفته کلود، دفترچه‌های کاری شامل بیش از دوازده موضوع در منطق و مبانی ریاضیات هستند که در بیش از ۸۰ سالی که از نگارششان گذشته، یافت نشده‌اند. پس این یک چیز برای کاوش است. اما موارد دیگری هم وجود دارد. دفترچه‌های فیزیک و کیهان‌شناسی او سرزمینی ناشناخته هستند که من قصد دارم پس از اتمام پروژه‌های فعلی منطقم، کاوش آن‌ها را آغاز کنم.»
جوئل دیوید همکینز، استاد منطق در دانشگاه نوتردام، ایندیانا، بازسازی اثبات استقلال بدیهی انتخاب توسط کلود را ندیده است، اما گفت اگر این اثبات صحیح باشد «شگفت‌انگیز و از نظر تاریخی جالب است. هرچند تشخیص اینکه چقدر مربوط به کلود و چقدر مربوط به گودل است، وظیفه‌ای برای مورخان است.»
همکینز گفت: «اینکه چیزهایی شبیه به [اثبات کوهن] در آنجا وجود دارد، به معنای داشتن آن اثبات نیست. این نشان می‌دهد او در مسیر درست بوده است. شما برای کاری که به کسی نمی‌گویید اعتباری کسب نمی‌کنید. اما گودل آنقدر ایده‌های انقلابی داشت که شاید تعجب‌آور نباشد که دفترچه‌هایش پر از چیزهای هیجان‌انگیز است.»