TL;DR

Logo Lean - ngôn ngữ chứng minh toán học hình thức

Lean Game Server tại adam.math.hhu.de là nền tảng mã nguồn mở hosting 8 game học toán hình thức (formal mathematics) ngay trên trình duyệt - không cần cài Lean, không cần tài khoản, hoàn toàn miễn phí. Bắt nguồn từ Natural Number Game của Kevin Buzzard tại Imperial College London, server hiện phủ từ số tự nhiên đến giải tích thực, đại số tuyến tính, lý thuyết tập hợp và logic hình thức. Giáo viên có thể tự build game riêng và publish lên server nhờ GameSkeleton template mã nguồn mở.

Từ "trò chơi" đến chứng minh toán học

Kevin Buzzard, giáo sư toán tại Imperial College London, nhận ra một vấn đề cốt lõi: máy tính không thể đọc toán học viết theo kiểu người dùng - kể cả với sự trợ giúp của AI và machine learning. Ông tạo ra Natural Number Game (NNG) cùng Mohammad Pedramfar để dạy người dùng viết chứng minh mà máy tính có thể kiểm tra được, thông qua ngôn ngữ Lean.

Ý tưởng rất đơn giản: thay vì nói "a + b = b + a là hiển nhiên vì bạn đổi chỗ hai nhóm viên bi", game yêu cầu bạn chứng minh điều đó từ các tiên đề Peano, bước-một-bước, theo cách mà máy tính chấp nhận. Kết quả: NNG trở thành cổng vào Lean cho hàng nghìn người dùng trên toàn cầu.

Khi cộng đồng chuyển sang Lean 4, Alexander Bentkamp và Jon Eugster tại Đại học Heinrich Heine Düsseldorf xây dựng Lean Game Server - một nền tảng mới với giao diện tốt hơn, nhiều game hơn, và khả năng tự chạy Lean ngay trong trình duyệt mà không cần cài đặt gì.

8 game, hàng trăm bài tập

Server hiện hosting 8 game với quy mô và chủ đề đa dạng:

  • Natural Number Game - 9 worlds, 79 levels: xây dựng N từ tiên đề Peano. Có bản dịch tiếng Anh, Trung, Ukraina, Ý, Pháp.
  • Real Analysis, The Game - 44 worlds, 139 levels: học giải tích thực qua các "khủng hoảng lịch sử" buộc toán học phải tái xây dựng calculus từ đầu thế kỷ 19.
  • Linear Algebra Game - 17 worlds, 158 levels: chứng minh bất đẳng thức Cauchy-Schwarz, không gian vector và tích trong dựa trên sách "Linear Algebra Done Right" của Axler.
  • Reintroduction to Proofs - 10 worlds, 88 levels: viết chứng minh theo ngôn ngữ dependent type theory, dành cho người muốn hiểu toán học hình thức từ nền tảng.
  • Set Theory Game: chứng minh các định lý về hợp, giao, phần bù tập hợp.
  • A Lean Intro to Logic: nhập môn logic mệnh đề xây dựng (constructive logic) trong Lean.
  • Knights and Knaves: giải bài toán logic "hiệp sĩ và kẻ nói dối" bằng Lean.
  • Scribble: khám phá toán học bậc đại học năm nhất qua elf thông minh tên Scribble.

Mỗi game được duy trì bởi chuyên gia riêng: Kevin Buzzard (NNG), Alex Kontorovich (Real Analysis), Emily Riehl (Reintroduction to Proofs), Dan Velleman (Set Theory).

Dưới nắp ca-pô

Game chạy bằng cách tải bản JavaScript của Lean engine về trình duyệt người dùng - server không phải xử lý từng keystroke. Phía server chạy Lean trong sandbox bubblewrap để bảo mật, với capacity khoảng 70 session đồng thời trên máy chủ của Đại học Düsseldorf.

Codebase lean4game trên GitHub: 452 stars, 84 forks, 38 contributors, 1.294 commits. Stack: TypeScript 62,4% + Lean 28,6%. Giấy phép GPL-3.0. Được tài trợ bởi chương trình Freiraum 2022 (Đức) và AI for Math Fund của Renaissance Philanthropy.

Muốn tự host? Có docs hướng dẫn đầy đủ từ cách chạy local đến deploy server riêng.

Ai nên thử ngay

  • Sinh viên toán năm nhất: học chứng minh hình thức song song với môn học, được feedback tức thì từ Lean engine.
  • Developer muốn hiểu proof assistant: không cần cài Lean, không cần biết toán chuyên sâu - NNG là điểm khởi đầu tốt nhất.
  • Giảng viên: dùng GameSkeleton template để xây game riêng cho môn học, publish lên server để sinh viên chơi trực tiếp trên trình duyệt.
  • Người quan tâm đến AI for Math: Lean là ngôn ngữ máy tính "hiểu" toán học - hiểu Lean nghĩa là hiểu tại sao việc dạy AI chứng minh định lý lại khó đến vậy.

Phía trước

NNG đang có kế hoạch mở rộng thêm khoảng 15 levels về quan hệ nhỏ hơn, dẫn đến chứng minh rằng N là ordered semiring và strong induction hoạt động. Về lâu dài: số chẵn/lẻ, số nguyên tố và phân tích thừa số. Cộng đồng đang tìm kiếm tình nguyện viên dịch các game sang ngôn ngữ chưa có.

Server vẫn đang trong giai đoạn phát triển tích cực. Gặp lỗi - mở GitHub Issue. Muốn thêm game của bạn - liên hệ nhóm phát triển.

Nguồn: Lean Game Server, leanprover-community/lean4game, @leanprover trên X.