Khoảng mười năm trước, Marijn Heule, Oliver Kullmann và Victor Marek đã chứng minh rằng nếu bạn tô màu 2 màu cho các số nguyên dương từ 1 đến 7825, thì bạn phải có thể tìm thấy x, y và z đều cùng màu với x^2+y^2=z^2 -- tức là, một bộ ba Pythagore đơn sắc. 1/

Điều này đã giải quyết một vấn đề cũ của Ron Graham. Bằng chứng là một lập luận brute-force khổng lồ. Không hoàn toàn là brute force, vì điều đó sẽ hoàn toàn không khả thi, mà là một phép tính brute-force thông minh sử dụng một SAT solver. 2/

Nhưng tôi khá chắc chắn rằng điều đó được nói một cách hài hước và không phải (như đã gợi ý trong bài viết của Quanta) như một loại chỉ trích nào, vì tôi nghĩ bây giờ, và đã nghĩ lúc đó, rằng những loại kết quả như thế này thật sự rất thú vị. 4/

Câu đùa sẽ là gợi ý rằng một người có thể đọc một chứng minh kiểu này như thể nó là một loại lập luận thông thường hơn, và các phân tích trường hợp phức tạp trong các lập luận thông thường thường được coi là hơi xấu xí. 5/

Nhưng tất nhiên, một bằng chứng kiểu này không được thiết kế để đọc theo cách thông thường, và có sức hấp dẫn riêng của nó. Cá nhân tôi, tôi không vấn đề gì với ý tưởng sử dụng những lập luận hay để giảm một bằng chứng thành một phép tính khổng lồ và sau đó thực hiện phép tính đó. 6/

Có vẻ như có một số vấn đề không thể giải quyết một cách thực tế ngoại trừ bằng cách tiếp cận này, trong trường hợp đó tôi không thấy lý do gì để không sử dụng nó, và tôi hài lòng với mức độ hiểu biết đạt được.

Nói như vậy, nếu ai đó tìm ra một bằng chứng cho định lý bốn màu (ví dụ) mà không cần phân tích nhiều trường hợp, tôi sẽ ăn mừng điều đó và coi đó là một bước tiến trong sự hiểu biết, vì nó sẽ giải thích tại sao phân tích trường hợp lại hoạt động.

điều mà bây giờ tôi coi là một điều chỉ đơn giản là như vậy. Tương tự, nếu ai đó tìm ra một lập luận có quy mô con người cho vấn đề bộ ba Pythagore thì tôi sẽ rất vui mừng. Nhưng tôi rất nghi ngờ rằng một lập luận như vậy tồn tại, và điều đó không làm tôi bận tâm.