欢迎来到 NyaOJ ^^

这里是 NyaOJ， 一个面向 Lean 的 OJ 喵！

我们实现了一个通用的 Lean 评测系统，不仅仅有基于 Lean 内核的证明验证，还内置了一个 @Vvauted 魔改的 UOJ 沙箱 Re-UOJ-Judger 同时支持了传统算法竞赛题的运行时验证，并且我们正计划实现一些工具来帮助对于算法竞赛题的证明。

我们目前支持了 4.23.0 版本的 Lean，预编译了 Mathlib 和 Loom 两个库。

欢迎加 QQ 群 (1084540391) 来玩！