เจาะลึก Atlas Theorem พิสูจน์ความสอดคล้องสถาปัตยกรรมซอฟต์แวร์ด้วย Lean 4

ภาพพอร์ตเทรตที่เหมือนจริงกับภาพพิกเซลอาร์ตขนาด 16×16 พิกเซล ต่างก็สื่อถึงใบหน้าเดียวกันได้ นักทฤษฎีการ์ตูน Scott McCloud เคยเรียกสิ่งนี้ว่าการขยายความผ่านการลดทอน (amplification through simplification) ซึ่งหมายถึงการตัดเส้นทิ้งไม่ได้ทำให้ข้อมูลสูญหาย แต่เป็นการขับเน้นแก่นแท้ให้ชัดเจนยิ่งขึ้น

คำถามคือเราสามารถพูดแบบเดียวกันกับการวินิจฉัยสถาปัตยกรรมซอฟต์แวร์ได้หรือไม่ หากเรามองระบบที่ระดับบริการ (service granularity) หรือระดับโมดูล (module granularity) บั๊กแบบเดียวกันจะปรากฏในจุดเดิมเสมอ โดยไม่ใช่แค่ความรู้สึกแต่เป็นข้อรับประกันที่พิสูจน์ได้

บทความนี้คือบันทึกการพิสูจน์ข้อรับประกันดังกล่าว ซึ่งเรียกว่าทฤษฎีบท Atlas (Atlas theorem) ใน Lean 4 โดยเอเจนต์ AI ที่ตั้งใจมาพิสูจน์กลับปฏิเสธเป้าหมายของตัวเองถึง 4 ครั้ง ซึ่งการปฏิเสธทั้งสี่ครั้งนั้นกลายเป็นส่วนที่ดีที่สุด หัวใจสำคัญไม่ใช่เทคนิคการพิสูจน์ แต่คือวินัยในการสะสมข้อผิดพลาดเหล่านี้เป็นผลลัพธ์แทนที่จะมองว่าเป็นความล้มเหลว

เหตุการณ์ทั้งหมดเกิดขึ้นระหว่างวันที่ 4 ถึง 8 สิงหาคม 2026 รวมเป็นเวลา 5 วันทำการ โดยมีหัวข้อหลักคือ AlgebraicArchitectureTheoryV2 ซึ่งใช้ซอร์สโค้ดเป็นแหล่งความจริง (source of truth) นำการใช้งานมาabstraction เป็นชิ้นส่วนที่เรียกว่า Atoms และเปลี่ยนข้อกำหนดเป็นสมการที่เรียกว่า laws จัดการสถาปัตยกรรมให้เป็นเรขาคณิตและวิเคราะห์ด้วยเรขาคณิตพีชคณิต ซึ่งนี่คือ AAT (Algebraic Architecture Theory) และ monorepo นี้คือการตรวจสอบอย่างเป็นทางการใน Lean 4

ภาพประกอบจากคลังภาพสต็อก ไม่ใช่ภาพจากเหตุการณ์จริง

ทฤษฎีนี้มีจุดอ่อนที่ทุกคนพยายามมองข้ามมาตลอด นั่นคือเรื่องของความละเอียด (granularity) เมื่อใดก็ตามที่คุณวิเคราะห์สถาปัตยกรรม คุณกำลังเลือกความละเอียดโดยปริยาย ไม่ว่าจะเป็นบริการ โมดูล หรือเมธอด หากการวินิจฉัยเปลี่ยนไปตามตัวเลือกนั้น สิ่งที่คุณกำลังวัดคือคุณสมบัติของสถาปัตยกรรมหรือความสะดวกของผู้สังเกตกันแน่