math/lean 4.35.0 OpenBSD

interactive and automated theorem prover

System: OpenBSD
Repository: OpenBSD ports
Maintainer: Kirill A. Korinsky <[email protected]>
Last update: 2026-10-16
Commit: 830d224cd7
Categories: math, lang

Description

Lean is an open source theorem prover and programming language. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.

Install

Binary package:

pkg_add lean

From the ports tree:

cd /usr/ports/math/lean && make install

Dependencies

Build dependencies 5

Run dependencies 1

devel/libuv

No port depends on this one.

Commit history 4

Date Commit Credits Log message

2026-10-16

830d224cd7

kirill

math/lean: update to 4.35.0

OK: tb@

2026-10-12 af505b7fca tb lean: drop maintainer

2026-09-19

25da7f1745

thfr

Implement get_exe_location with getexecpath(3), functionally aequivalent with other OS' implementations, instead of previous hard-coded + SUBST_CMD workaround.

ok tb@ (maintainer)

2026-08-26

7ade432ef9

lean: mark broken on mips64 and sparc64.

I don't think it ever built on mips64 and it didn't like the switch to clang on sparc64.