NEAR AI is now #1 on Lean Eval v1, Lean FRO's active benchmark of extremely hard formalization problems.

The system runs almost entirely on open-weight DeepSeek V4.1 Flash, so it's low cost and has no third-party model dependency.

This work lays the groundwork for formally verifying NEAR Protocol and core contracts, and for a tool any team can use to verify its own.