مسار · رحلةٌ مُرشَدة
البرهانُ يصير حَوسبة
الاكتشافُ البطيءُ أنَّ البرهانَ والبرنامجَ شيءٌ واحد، من قواعد غنتسن إلى مساعدات البرهان اليوم.
- 01
بصيرةُ غنتسن
حذفُ القطعيُظهِر غنتسن أنَّ للبرهان بنية: حذفُ القطع يحوّل أيَّ برهانٍ إلى برهانٍ مباشرٍ بلا التفاف. ويبدو أنَّ البرهانَ يمكن أن «يُشغَّل»: يُبسَّط خطوةً خطوة.
- 02
تشرتش وتورنغ
عدمُ قابلية مسألةِ التوقّف للبَتّاستقلالًا، يحدِّد حسابُ لامدا عند تشرتش وآلةُ تورنغ معنى «القابل للحوسبة» بدقّة، ويُظهران أنَّ بعض الأسئلة لا تُجيب عنها حوسبة.
- 03
التطابُق: كَري–هاوَرد
تناظرُ كَري–هاوَردالكشف: القضايا أنماط، والبراهينُ برامج. أن تبرهن قضيةً هو أن تكتب برنامجًا من نمطٍ بعينه. فالمنطقُ والحوسبةُ بنيةٌ واحدة.
- 04
أساسُ مارتن-لوف
نظريةُ الأنماط الحدْسية 1984يبني مارتن-لوف على هذا أساسًا كاملًا: نظريةَ الأنماط التابعة، حيث تُمارَس الرياضياتُ ببناء الكائنات، والبرهانُ برنامجٌ يمكن فحصُه.
- 05
إلى داخل الآلة
المنطق الحاسوبياليومَ صار التناظرُ ملموسًا: لين وكوك وأغدا لغاتٌ يكتب بها الرياضيّون براهينَ يفحصها الحاسوب، ويعين أحيانًا على اكتشافها.