ปัญหาด้านการสอนในคณิตศาสตร์ขั้นสูง
(susam.net)- การอธิบายที่ ไม่ดีพอ ในคณิตศาสตร์ระดับประถมและมัธยมอาจทำให้นักเรียนถอยห่างจากคณิตศาสตร์ และลงเอยด้วยการเหลืออยู่เพียงนักเรียนที่มีแรงจูงใจสูงมากเท่านั้น
- บทพิสูจน์จำนวนมากในตำราคณิตศาสตร์ขั้นสูงมีลักษณะใกล้เคียงกับ ภาพรวมระดับสูง มากกว่าจะเป็นบทพิสูจน์ที่สมบูรณ์ ทำให้นักเรียนต้องเติมเหตุผลรองรับของแต่ละบรรทัดด้วยตนเอง
- ใน Galois Theory ของ Stewart การคลี่คลายข้อโต้แย้งในกรณีหนึ่งโดยเฉพาะใช้เวลาถึงสองวัน และแม้แต่นักคณิตศาสตร์อาชีพก็ยังเห็นว่าขั้นตอนระหว่างทางคลุมเครือ
- หากใส่รายละเอียดทั้งหมดลงไป ตำรา 200 หน้า อาจกลายเป็น 2000 หน้าได้ จึงเลี่ยงการละบางส่วนไม่ได้ แต่จำนวนและขนาดของสิ่งที่ถูกละไว้มีมากจนชวนทรมาน
- จำเป็นต้องมีแหล่งข้อมูลอย่างบันทึกประกอบของมหาวิทยาลัยชั้นดี ที่ขยายข้อโต้แย้งยาก ๆ ให้เป็นทั้ง บทพิสูจน์ที่เคร่งครัด และคำอธิบายเชิงสัญชาตญาณ และมีแผนจะทำบันทึกเสริมสำหรับบางหัวข้อก่อน
ช่องว่างของคำอธิบายที่ปรากฏในการศึกษาคณิตศาสตร์ขั้นสูง
- การอธิบายที่ ไม่ดีพอ ในการเรียนคณิตศาสตร์ระดับประถมและมัธยมอาจทำให้นักเรียนห่างจากคณิตศาสตร์ไปตลอดชีวิต และอาจทำให้เหลือเพียงผู้ที่มีแรงจูงใจสูงมากเท่านั้นที่เรียนต่อ
- คณิตศาสตร์มักถูกมองว่าเป็นวิชาที่ฝึก ความเคร่งครัดของการให้เหตุผล ความชัดเจนของความคิด และการสร้างข้อโต้แย้งจากหลักการพื้นฐาน
- ปัญหาคล้ายกันนี้ยังต่อเนื่องมาถึงคณิตศาสตร์ขั้นสูง โดยบทพิสูจน์ในตำราระดับบัณฑิตศึกษาหลายเล่มใกล้เคียงกับ ภาพรวมระดับสูง มากกว่าจะเป็นบทพิสูจน์ที่สมบูรณ์
- เมื่อตำราไม่แสดงขั้นตอนระหว่างทางอย่างเพียงพอ นักเรียนต้องใช้ความพยายามมากในการทำความเข้าใจและหาเหตุผลรองรับของแต่ละบรรทัด
- ข้อโต้แย้งยาว 10 บรรทัด ในตำราบางเล่ม เมื่อนำมาเขียนคลี่ออกเป็นบทพิสูจน์ที่น่าเชื่อถือแล้ว อาจยาวได้ถึง 10 หน้า
การละรายละเอียดในตำราและความจำเป็นของสื่อเสริม
- ต่อให้ขัดเกลาขั้นตอนระหว่างทางของตำราร่วมกับนักคณิตศาสตร์อาชีพแล้ว ขั้นตอนกลางของบทพิสูจน์บางชิ้นก็ยังคลุมเครือแม้แต่นักคณิตศาสตร์อาชีพเอง
- ใน Galois Theory ของ Stewart การคลี่คลายข้อโต้แย้งที่ซับซ้อนของกรณีหนึ่งใช้เวลาสองวัน และผลลัพธ์ต้องตอบโจทย์ทั้งความถูกต้อง ความสมบูรณ์ และการเข้าถึงได้สำหรับนักเรียนที่มีแรงจูงใจเพียงพอ
- มุกอย่าง ‘proof by obviousness’ และ ‘proof by intimidation’ ใช้กันได้ก็เพราะในตำราจริงมีสถานการณ์แบบนั้นปรากฏอยู่บ่อยครั้ง
- ปัญหาไม่ได้อยู่แค่การละผลลัพธ์พื้นฐานระดับปริญญาตรีอย่างทฤษฎีกลุ่มหรือทฤษฎีสนามเท่านั้น แต่คือแม้จะสมมติว่านักเรียนรู้เนื้อหาระดับปริญญาตรีทั้งหมดแล้ว ก็ยังไม่เห็นชัดเพียงพอว่าทำไมบทพิสูจน์ในตำราระดับบัณฑิตศึกษาจึงใช้ได้
- นักเรียนต้องเรียนหัวข้อต่าง ๆ ให้ทันกำหนดเวลาที่มีจำกัด ดังนั้นหากคำอธิบายในตำราไม่เพียงพอ ก็ไม่มีเวลาพอที่จะคลี่ข้อโต้แย้ง 10 บรรทัดทุกอันให้เป็นบทพิสูจน์ 10 หน้าได้ด้วยตนเอง และอาจไม่มีวันได้เรียนรู้เหตุผลที่แท้จริงอย่างครบถ้วน
- ในงานวิจัยปัญหานี้ยิ่งรุนแรงกว่า แต่ในที่นี้จะเน้นที่ตำรา
- ตำราขั้นสูงเองก็มีข้อจำกัดในทางปฏิบัติที่ไม่อาจให้เหตุผลรองรับทุกข้อโต้แย้งได้
- หากใส่รายละเอียดทั้งหมดลงไป ตำรา 200 หน้า อาจกลายเป็น 2000 หน้าได้
- ทั้งนักเรียนและอาจารย์ต่างก็ไม่มีเวลาหรือความอดทนพอจะอ่านข้อโต้แย้งเชิงเทคนิคหลายพันหน้าที่ไม่น่าสนใจ
- ผู้เขียนจึงมักโฟกัสที่ส่วนที่น่าสนใจ และคาดหวังให้นักเรียนเติมส่วนที่ละไว้เอง
- ถึงอย่างนั้น จำนวนและขนาดของสิ่งที่ถูกละไว้ในตำราทั่วไปก็ยังมีมากจนชวนทรมาน
- มหาวิทยาลัยดี ๆ หลายแห่งมีบันทึกประกอบที่ช่วยขยายข้อโต้แย้งยาก ๆ ให้เป็นทั้ง บทพิสูจน์ที่เคร่งครัด และคำอธิบายเชิงสัญชาตญาณ ซึ่งดูเป็นแนวปฏิบัติที่ดี
- ตำราระดับบัณฑิตศึกษานั้นดีกว่าไม่มีเลยมาก เพราะอย่างน้อยก็ทำให้หัวข้อต่าง ๆ ถูกเผยแพร่ออกสู่โลก แต่ก็ยังมีข้อจำกัดตรงที่แหล่งข้อมูลเหล่านี้เข้าถึงได้ยากอยู่บ่อยครั้ง
- หากมีเวลาไม่จำกัด ก็อยากทำสื่อเสริมที่คลี่ข้อโต้แย้งทั้งหมดในตำราเหล่านี้อย่างละเอียด แต่ในความเป็นจริงเป็นไปไม่ได้
- ถึงอย่างนั้นก็มีแผนจะเริ่มทำบันทึกเสริมจากหัวข้อที่รู้สึกว่าคุณภาพของคำอธิบายสำคัญเป็นพิเศษก่อน โดยยกตัวอย่างเช่น s-arc transitivity ของกราฟ และหัวข้อที่เกี่ยวข้องกับการขยายสนาม
1 ความคิดเห็น
ความคิดเห็นจาก Lobste.rs
โอ้ อันนี้เจ็บเลย ขอเล่าเกร็ดส่วนตัวปนบ่นหน่อยว่า หนึ่งในเหตุผลที่ผันตัวไปทำ software engineering แทนคณิตศาสตร์/วิทยาการคอมพิวเตอร์ ก็คือ ช่องว่างในการเข้าใจคณิตศาสตร์ ระหว่างตอนฟังในห้องเรียนกับตอนอ่านหนังสือเองมันใหญ่มาก
ผมใช้เวลามากผิดปกติกว่าจะเข้าใจทฤษฎีบทที่เขียนเป็นลายลักษณ์อักษร และพอสุดท้ายเข้าใจแล้วก็มักรู้สึกว่าเนื้อหาที่จริง ๆ ง่ายนั้นถูกอธิบายในแบบที่ไม่เข้าท่ากับรสนิยมของผมเอามาก ๆ จนรู้สึกไม่พอใจ
แต่ผมวินิจฉัยปัญหาต่างออกไปนิดหน่อย ไม่ใช่ว่ารายละเอียดน้อยเกินไป ตรงกันข้าม ผมคิดว่าปัญหาคือขาด แรงจูงใจและภาพรวม มากกว่า พิสูจน์ต่าง ๆ ดูเหมือนถูกเขียนแบบย้อนกลับหมด คือคิดปัญหาอยู่นานจนเจอพิสูจน์ แล้วลบกระบวนการคิดทิ้ง จากนั้นเริ่มเขียนพิสูจน์จากขั้นตอนสุดท้าย
ตัวอย่างเช่น พิสูจน์มักเริ่มด้วย “ให้เลือก ɛ = n^2 / 36” แล้วเราต้องอ่านรอบหนึ่งเพื่อดูว่าทำไม epsilon ตัวนั้นถึงจำเป็นในเชิงกลไก จากนั้นต้องคิดต่ออีกเพื่อเข้าใจไอเดียที่อยู่หลังกลวิธีทางเทคนิคนั้น แล้วลองพิสูจน์แบบไม่เป็นทางการในหัวด้วยไอเดียนั้น สุดท้ายค่อยกลับมาอ่านอีกครั้งโดยมีไอเดียนั้นอยู่ในใจเพื่อดูว่าพิสูจน์นี้เป็นการทำให้เป็นทางการที่ถูกต้องหรือไม่ การทำให้เป็นทางการมีประโยชน์ แต่ไม่ใช่ตัวความเข้าใจเอง
Reed-Solomon ก็เป็นตัวอย่างได้ Wiki อาจพูดง่าย ๆ ว่า “พหุนามดีกรี N สามารถอินเตอร์โพเลตได้จากจุด N+1 จุด ถ้าส่งจุด K จุดซ้ำเผื่อไว้ ต่อให้หายไปบางส่วนก็ยังกู้ค่าสัมประสิทธิ์กลับมาได้” แต่กลับเลือกอธิบายแบบยืดยาวและเข้าใจยากแทน (previously)
ตัวอย่างล่าสุดคือทฤษฎีบท 1.5.8 ใน Analysis ของ Tao ซึ่งบอกว่าเซตกะทัดรัดทุกเซตมีคุณสมบัติที่ open cover ทุกอันมี finite subcover เขาเข้าสู่เรื่องทันทีด้วย “เลือก y, เลือก V_a, มีบอลหนึ่งลูก, มีรัศมี r...” ซึ่งก็ไม่ผิดหรอก แต่ยากจะเห็นว่าทำไปทำไม
กว่าจะซึมซับรูปแบบทางการได้ก็ถึงจะเห็นไอเดียแกนกลาง เราต้องการ finite subcover ดังนั้นการเลือกเซตที่ “ใหญ่ที่สุด” แบบละโมบจึงดูเป็นธรรมชาติ แต่ต้องนิยามก่อนว่าใหญ่ที่สุดหมายถึงอะไร ถ้าตรึงจุดหนึ่งไว้ เราก็เลือกเซตที่ใหญ่ที่สุดเมื่อเทียบกับจุดนั้นได้ และขยายบอลไปเรื่อย ๆ จนเหลือสมาชิกของ cover เพียงตัวเดียว บอลจะเล็กลงได้ไม่สิ้นสุดไม่ได้ แล้วจากตรงนั้นก็ใช้ความกะทัดรัดเพื่อเลือกจุดที่มีบอลรัศมี 0 ได้ เพราะฉะนั้นบอลต้องกว้างอย่างน้อย ɛ หนึ่งค่า แล้วเราก็เลือกเซตที่ใหญ่ที่สุดต่อไปสำหรับจุดที่ยังไม่ถูกคลุม ถ้าจบในจำนวนขั้นตอนจำกัดก็สำเร็จ ถ้าไม่จบก็จะได้ลำดับของจุดที่ห่างกันอย่างน้อย ɛ ซึ่งขัดกับความกะทัดรัด
ไอเดียหลักมักง่ายกว่าการทำให้เป็นทางการมาก และพอจับมันได้แล้ว ก็จะรู้สึกว่าถ้าขัดเกลาอสมการให้พอ การทำให้เป็นทางการบางแบบย่อมเป็นจริงแน่ ๆ การทำให้เป็นทางการก็ยังจำเป็นอยู่ เราอาจเผลอพึ่งพา something อย่างสัจพจน์การเลือกโดยไม่รู้ตัวก็ได้ แต่ในฐานะเครื่องมือสื่อสารไอเดีย มันแย่มาก เหมือน ไล่แกะ quicksort จาก assembly code ย้อนกลับ
ผมคิดว่าวิธีนำเสนอคณิตศาสตร์ที่ถูกต้องคือไม่เอาทฤษฎีบทเป็นจุดเริ่มต้น แต่เอาเป็นผลลัพธ์ แล้วอธิบายในโหมดว่า “เราน่าจะค้นพบสิ่งนี้ได้อย่างไร”
แน่นอน ผมไม่ได้ปฏิเสธว่าบางครั้งก็มีข้อโต้แย้งแบบ “ต้องจับเขย่าจนกว่าจะยอมรับจริง ๆ ว่านี่พิสูจน์ได้” อยู่เหมือนกัน แต่ในคณิตศาสตร์ที่ค่อนข้างไม่โหดที่ผมเคยเจอ กรณีแบบนั้นมีไม่บ่อยนัก
ทฤษฎีบทในตำราเหมือนภาพเค้กสำเร็จรูปในหนังสือทำอาหาร ส่วนพิสูจน์ก็เหมือนสูตร ขณะที่ความเละเทะระหว่างทำเค้กจริง ๆ กลับแทบมองไม่เห็น
สิ่งที่หายไปคือ ต่อให้มีสูตร คุณก็ยังต้องมี ความเข้าใจและทักษะด้านการอบ ถึงจะทำเค้กแบบเดียวกันได้ ในสูตรอาจไม่มีเรื่องอย่างความข้นของแป้ง หรือควรแก้อย่างไรเมื่อทำพลาด และการรู้ “หลักการพื้นฐาน” ของการอบก็ไม่ได้ทำให้คุณกลายเป็นคนทำขนมปังทันที คุณอาจมีไอเดียพื้นฐาน แต่ก็ยังต้องเอามันมาประกอบกันเพื่ออบเค้ก
ผมว่าคณิตศาสตร์ก็เหมือนศาสตร์สมัยใหม่อื่น ๆ ตู้โชว์เต็มไปด้วยเค้ก และคนทำขนมชั้นยอดก็ได้รับทุนวิจัยเพื่ออบเค้กเพิ่มอีก ถ้าอยากเป็นคนทำขนมเอง คุณต้องไปฝึกงานในร้านเพื่อเรียนรู้เคล็ดลับ แล้วเริ่มทำเค้กของตัวเองแทนที่จะใช้แต่สูตรของหัวหน้า เรื่องนี้ต้องใช้เวลา ความพยายาม และโชคนิดหน่อย
https://betterexplained.com/articles/…
ลำดับ DNA อาจเป็นคำอธิบายแมวที่แม่นยำมาก แต่ดูแค่นั้นอย่างเดียวก็ยังนึกภาพสัตว์ตัวนั้นในหัวไม่ได้
การจัดรูปแบบแบบนี้ทำให้การตรวจสอบและการแก้ไขมีประสิทธิภาพกว่า และเรียกสิ่งนี้ว่า มุมมองแบบ BCH ของ R-S แม้ว่า BCH เองก็เป็นชื่อของตระกูลโค้ดทั้งกลุ่มด้วย
ถึงอย่างนั้นก็เห็นด้วยว่า แม้จะอ่านเรื่องนี้เยอะมากตอนลงมือ implement แล้ว บทความ Wikipedia เกี่ยวกับ R-S และ BCH ก็ยังแทบเข้าใจไม่ได้อยู่ดี ถ้าไม่มีไลบรารี gf256 แบบ literate programming ที่ยอดเยี่ยม โดยเฉพาะ gf256::rs ผมคงไปต่อไม่ได้
อย่างไรก็ตาม จากประสบการณ์ของผม บางทฤษฎีบทพิสูจน์ง่ายกว่าอีกหลายอัน ในวิชา Algebra I การสอบครั้งหนึ่งคือให้พิสูจน์ทฤษฎีบทอะไรก็ได้ที่อาจารย์เลือกขึ้นมาสด ๆ ฟังดูน่ากลัว แต่พอคุณอยู่กับการพิสูจน์สิ่งที่พิสูจน์แล้วมานานพอ คุณจะเริ่มมองเห็น รูปแบบ และคุณยังจำทฤษฎีบทที่ถูกใช้ในพิสูจน์อื่น ๆ ได้มากขึ้นด้วย
ไม่ได้บอกว่าง่ายนะ แต่การเรียนคณิตศาสตร์ในระดับนั้นจะให้ความรู้สึกเหมือนมีอะไรบางอย่างเปิดออกในหัวจนมันกลายเป็นสิ่งที่ทำได้ การทำให้เป็นทางการอาจดูมากเกินไป แต่ก็นี่เองที่ทำให้นักคณิตศาสตร์ไปถึงข้อสรุปที่คนอื่นมองไม่เห็นได้
จากประสบการณ์ส่วนตัวในสายวิทยาศาสตร์กายภาพ ผมคิดว่าหลายอย่างมาจาก วิธีที่บทความวิชาการถูกเขียน ตีพิมพ์ และประเมิน
กระบวนการเขียนและตีพิมพ์บทความไม่ได้ผลักดันให้คนอธิบายวิทยาศาสตร์จริง ๆ แต่ผลักให้พูดอะไรที่ดูน่าเชื่อถือและชวนเชื่อนิด ๆ โดยไม่ “เสีย” เวลากับรายละเอียดมากเกินไป อคติแบบนี้ที่เห็นในงานพิสูจน์ก็ดูคล้ายกันมาก
ควรถอดสำนักพิมพ์ออกจากวิทยาศาสตร์
ถ้าจะอธิบายว่า “ค้นพบสิ่งนี้ได้อย่างไร” คุณต้องพูดข้อความกำกวม หยาบ ๆ ที่ยังไม่ได้ให้เหตุผลครบถ้วนหรือไม่แม่นยำเต็มที่ ผู้ประเมิน ไม่ว่าจะเป็น proceedings ของงานประชุมที่ตีพิมพ์เองแต่มีการทำดัชนี หรือ overlay journal ก็ตาม มักไม่ชอบให้ประโยคที่ออกจะไม่จริงอยู่บ้างหลงเหลือในฉบับสุดท้ายที่รับตีพิมพ์
เพราะอย่างนั้น ต่อให้ต้นฉบับแรกมี คำอธิบายเชิง intuition อยู่ มันก็มักถูกตัดออกในตอนท้าย
แถมยังมีกรณีที่แย่กว่าอีก ผู้เขียนร่วมของผมคนหนึ่งที่เก่งมากทั้งเรื่องเขียนบทนำและปรับงานให้มีโอกาสรับตีพิมพ์ เขามักอธิบายว่าเวลาเลือกเวอร์ชันของข้อความตั้งต้น มันมักมี trade-off เวอร์ชันที่ถูกรับตีพิมพ์ง่ายที่สุดมักกลับเป็นเวอร์ชันที่แย่ที่สุดสำหรับคนที่จะชอบและอ้างอิงบทความนั้น ทั้งที่ทุกเวอร์ชันล้วนเป็นจริงและพิสูจน์ได้ด้วยคุณภาพของพิสูจน์ระดับเดียวกันก็ตาม
เพราะอย่างนั้นแรงจูงใจจึงไม่สอดคล้องกัน แต่ครั้งนี้อาจไม่ใช่ความผิดของสำนักพิมพ์เท่าไร อาจเป็นเพราะโครงสร้างที่นักวิชาการไม่ได้รับรางวัลจากงานที่ควรทำจริง ๆ แต่ได้รับรางวัลจากตัวชี้วัดการตีพิมพ์แทน
สำหรับตำรา ผมไม่แน่ใจว่าจะเห็นด้วยกับข้อกล่าวหาในโพสต์เต็ม ๆ การละบางอย่างไว้อย่างดีอาจทำให้พิสูจน์อ่านง่ายขึ้นและกระตุ้นให้ผู้อ่านคิดตามได้ด้วย ในกรณีแย่สุดก็ไปดูตำราเล่มอื่นหรือแหล่งต้นฉบับได้ แต่ถ้าเจอพิสูจน์ไม่ครบในบทความวิจัย มันชวนหงุดหงิดมาก เพราะตรงนั้นความสงสัยจะเริ่มแทรกเข้ามาว่ามีใครถือพิสูจน์ฉบับเต็มอยู่จริงหรือเปล่า และพอรู้ตัวอีกทีอาจผ่านไปเป็นสัปดาห์/เดือน/ปีแล้วก็ได้
ในฐานะนักศึกษาปริญญาโทด้านคณิตศาสตร์ ผมคิดว่าปัญหานี้มีสองด้าน บางครั้งพิสูจน์ที่นำเสนอก็อยู่ในระดับสูงพอสมควรจนถ้าติดขั้นตอนใดขั้นตอนหนึ่งจริง ๆ ก็ชวนหงุดหงิด แต่ในทางกลับกัน กระบวนการเติมช่องว่าง บางทีก็มีประโยชน์ต่อการพัฒนาทักษะมากกว่าการได้รับทุกอย่างครบถ้วน
ถ้าพิสูจน์กระโดดจากข้อความตั้งต้น 1 ไปข้อความตั้งต้น 2 แล้วคุณยังไม่เข้าใจทันที อย่างแรก มันช่วยให้คุณมี intuition ว่าผู้เขียนและชุมชนนักคณิตศาสตร์ในสาขานั้นมองอะไรว่าเป็นเรื่อง obvious ซึ่งมีคุณค่าเพราะมันบอกว่าผลลัพธ์แบบไหนที่คุณควรทำให้คุ้นเคยอย่างลึกซึ้งในเชิง intuition
อย่างที่สอง ถ้าคุณเติมขั้นกลางเองและทำให้ตัวเองเชื่อได้ว่าข้อโต้แย้งนั้นแน่นพอ คุณจะจำขั้นกลางนั้นได้ดีกว่าการที่มันถูกพิมพ์มาให้บนหน้ากระดาษเสียอีก
สำหรับผม “จุดพอดี” คือเวลาที่ใช้ให้เหตุผลกับขั้นตอนหนึ่งของพิสูจน์อยู่ราว 30 วินาทีถึง 5 นาที ถ้านานกว่านั้นก็มักจะหงุดหงิดและเรียนรู้ได้แย่ลง
รอจนกว่าคุณจะได้เห็นพิสูจน์ในบทความจริงก่อนเถอะ
เอาจริง ๆ ก็แน่นอนว่ามีตำราคณิตศาสตร์ที่เขียนไม่ดีและไม่เหมาะกับการสอนอยู่ แต่ผมคิดว่าพิสูจน์ระดับบัณฑิตศึกษาโดยเฉลี่ยนั้นเขียนรายละเอียดทุกอย่างลงไปหมดไม่ได้ เพราะถ้าทำแบบนั้นจะอ่านเหนื่อยและน่าเบื่ออย่างยิ่ง
นักคณิตศาสตร์ถูกคาดหวังให้ อุดช่องโหว่ของพิสูจน์ ในหัวเอง และความสามารถนี้ก็เป็นสิ่งที่ต้องเรียนรู้
ผมมีเกร็ดส่วนตัวเกี่ยวกับการเติมช่องว่างอยู่บ้าง
ตอนมัธยม หลังจากเถียงกันเรื่องระดับรายละเอียดที่ต้องการแล้ว เราตกลงกันว่าผมจะเขียนพิสูจน์แบบละให้น้อยที่สุด ถ้าผมแสดงให้เห็นได้ว่าผมเติมช่องว่างเองได้ ก็จะยอมรับว่าข้อความจำนวนมากที่เขียนแบบเป็นเพียงโครงร่างมากกว่าที่คาด ก็เพียงพอจะพิสูจน์ความเข้าใจที่ต้องการแล้ว
ผมยังจำได้ว่ามีวงเล็บซ้อนอย่างน้อยสามชั้นแบบ “จริง ๆ ตรงนี้ไม่ต้องมีพิสูจน์ชัด ๆ แต่เราตกลงกันไว้แล้ว” วงเล็บชั้นล่างสุดอันหนึ่งมีข้อความว่า “มาพิสูจน์ด้วยอุปนัยว่า
2^n>0” ส่วนข้อความตั้งต้นด้านบนสุดน่าจะเกี่ยวกับลิมิต และขอเสริมว่าเราต่างก็เห็นตรงกันว่าพิสูจน์ระดับล่างสุดที่เยิ่นเย้อเหล่านั้นเยิ่นเย้อเกินไปจริง ๆตอนจดเลกเชอร์ทั้งในมัธยมและมหาวิทยาลัย ผมมักเขียนใจความของสิ่งที่จะพูดต่อไปไว้ล่วงหน้า เพื่อซื้อเวลาให้ตัวเองเมื่อเนื้อหาถัดไปต้องจดรายละเอียดมากขึ้น ต่อมาพอเป็น postdoc ครั้งหนึ่งผมฟังเพื่อนร่วมงานอธิบายปัญหาหนึ่งอยู่ แล้วเผลอขัดขึ้นมาว่า “ข้ามส่วนนั้นไปได้เลย ผมเห็นแล้วว่าคุณกำลังจะพูด lemma อะไรและจะพิสูจน์ยังไง”
ปรากฏว่าผิด พวกเขาไม่ได้กำลังอ้างผลลัพธ์ แต่กำลังตั้งคำถามอยู่ต่างหาก ถึงอย่างนั้นพิสูจน์ที่ออกมาจากโครงร่างที่ผมเดาไว้ก็ลงเอยไปอยู่ในบทความจริง ๆ
ในหมู่คนที่ทำคณิตศาสตร์เชิงรูปธรรมแบบพวกเรา มีอีกโลกหนึ่งที่พยายามแก้ปัญหารายละเอียดด้วย proof assistant อย่าง Lean, Agda, Coq แต่ดูเหมือนแทบไม่มีใครใช้ proof assistant สำหรับสอนคณิตศาสตร์แบบ “ทั่วไป” เลย ทำไมกันนะ?
สำหรับคณิตศาสตร์ต่อเนื่อง มี ความไม่ตรงกันด้านการแทนความ อยู่บ้างระหว่างรูปแบบการเขียนมาตรฐานกับ proof assistant แบบตรรกะลำดับสูง ถ้าจะไปให้ไกลพอด้วยการทำให้เป็นทางการด้วยทฤษฎีเซตลำดับหนึ่ง ก็ต้องมีนิยามที่จำเป็นหลายอย่าง ซึ่งดูเหมือนยังไม่ได้ถูกรวบรวมเป็นชุดที่สอดคล้องกันนัก