math/lean4 4.35.0 FreeBSD

Theorem prover and functional language for math (new gen)

System: FreeBSD
Repository: FreeBSD ports
Maintainer: [email protected]
Last update: 2026-10-13
Commit: 9bcf1534aa
License: APACHE20
Categories: math, lang, devel

Description

Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean 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. The mathematical components library mathlib for Lean is being developed at Carnegie Mellon University.

In the other systems

System

Port

Version

FreeBSD

math/lean4

4.35.0

NetBSD

math/lean4

4.33.1nb1

Install

Binary package:

pkg install lean4

From the ports tree:

cd /usr/ports/math/lean4/ && make install clean

To depend on this port in another port's Makefile:

RUN_DEPENDS=	lean4>0:math/lean4

Packages

The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.

Repository	aarch64	amd64	armv6	armv7	i386
FreeBSD:14:latest	-	-	-	-	-
FreeBSD:14:quarterly	-	-	n/a	-	-
FreeBSD:15:latest	4.35.0	4.35.0	n/a	-	-
FreeBSD:15:quarterly	4.34.1	4.34.1	n/a	n/a	n/a
FreeBSD:16:latest	4.34.1	4.35.0	n/a	n/a	n/a
FreeBSD:16:quarterly	n/a	n/a	n/a	n/a	n/a

Dependencies

As this port's Makefile names them.

Build 3

bash : shells/bash
cadical : math/cadical
leantar : math/leangz

Library 2

libgmp.so : math/gmp
libuv.so : devel/libuv

Runtime 2

cadical : math/cadical
leantar : math/leangz

Test 3

bash : shells/bash
git : devel/git
gtail : sysutils/coreutils

The full lists below include those, and their dependencies in turn.

Build dependencies 22

Run dependencies 7

No port depends on this one.

Configuration

Options name: math_lean4

Option

Default

Description

MIMALLOC

off

Use mimalloc memory allocator (enables some optimizations in the code)

USES: cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build
Service scripts: none

Files

pkg-plist 17843

bin/lake
bin/lean
bin/leanc
bin/leanchecker
bin/leanexport
bin/leanir
bin/leanmake
include/lean/config.h
include/lean/lean.h
include/lean/lean_gmp.h
include/lean/lean_libuv.h
include/lean/mimalloc.h
include/lean/version.h
lib/lean/Init.ilean
lib/lean/Init.ir
lib/lean/Init.ir.sig
lib/lean/Init.olean
lib/lean/Init.olean.private
lib/lean/Init.olean.server
lib/lean/Init/BinderNameHint.ilean
lib/lean/Init/BinderNameHint.ir
lib/lean/Init/BinderNameHint.ir.sig
lib/lean/Init/BinderNameHint.olean
lib/lean/Init/BinderNameHint.olean.private
lib/lean/Init/BinderNameHint.olean.server
lib/lean/Init/BinderPredicates.ilean
lib/lean/Init/BinderPredicates.ir
lib/lean/Init/BinderPredicates.ir.sig
lib/lean/Init/BinderPredicates.olean
lib/lean/Init/BinderPredicates.olean.private
lib/lean/Init/BinderPredicates.olean.server
lib/lean/Init/ByCases.ilean
lib/lean/Init/ByCases.ir
lib/lean/Init/ByCases.ir.sig
lib/lean/Init/ByCases.olean
lib/lean/Init/ByCases.olean.private
lib/lean/Init/ByCases.olean.server
lib/lean/Init/CbvSimproc.ilean
lib/lean/Init/CbvSimproc.ir
lib/lean/Init/CbvSimproc.ir.sig
lib/lean/Init/CbvSimproc.olean
lib/lean/Init/CbvSimproc.olean.private
lib/lean/Init/CbvSimproc.olean.server
lib/lean/Init/Classical.ilean
lib/lean/Init/Classical.ir
lib/lean/Init/Classical.ir.sig
lib/lean/Init/Classical.olean
lib/lean/Init/Classical.olean.private
lib/lean/Init/Classical.olean.server
lib/lean/Init/Coe.ilean
lib/lean/Init/Coe.ir
lib/lean/Init/Coe.ir.sig
lib/lean/Init/Coe.olean
lib/lean/Init/Coe.olean.private
lib/lean/Init/Coe.olean.server
lib/lean/Init/Control.ilean
lib/lean/Init/Control.ir
lib/lean/Init/Control.ir.sig
lib/lean/Init/Control.olean
lib/lean/Init/Control.olean.private
lib/lean/Init/Control.olean.server
lib/lean/Init/Control/Basic.ilean
lib/lean/Init/Control/Basic.ir
lib/lean/Init/Control/Basic.ir.sig
lib/lean/Init/Control/Basic.olean
lib/lean/Init/Control/Basic.olean.private
lib/lean/Init/Control/Basic.olean.server
lib/lean/Init/Control/Do.ilean
lib/lean/Init/Control/Do.ir
lib/lean/Init/Control/Do.ir.sig
lib/lean/Init/Control/Do.olean
lib/lean/Init/Control/Do.olean.private
lib/lean/Init/Control/Do.olean.server
lib/lean/Init/Control/EState.ilean
lib/lean/Init/Control/EState.ir
lib/lean/Init/Control/EState.ir.sig
lib/lean/Init/Control/EState.olean
lib/lean/Init/Control/EState.olean.private
lib/lean/Init/Control/EState.olean.server
lib/lean/Init/Control/Except.ilean
lib/lean/Init/Control/Except.ir
lib/lean/Init/Control/Except.ir.sig
lib/lean/Init/Control/Except.olean
lib/lean/Init/Control/Except.olean.private
lib/lean/Init/Control/Except.olean.server
lib/lean/Init/Control/ExceptCps.ilean
lib/lean/Init/Control/ExceptCps.ir
lib/lean/Init/Control/ExceptCps.ir.sig
lib/lean/Init/Control/ExceptCps.olean
lib/lean/Init/Control/ExceptCps.olean.private
lib/lean/Init/Control/ExceptCps.olean.server
lib/lean/Init/Control/Id.ilean
lib/lean/Init/Control/Id.ir
lib/lean/Init/Control/Id.ir.sig
lib/lean/Init/Control/Id.olean
lib/lean/Init/Control/Id.olean.private
lib/lean/Init/Control/Id.olean.server
lib/lean/Init/Control/Lawful.ilean
lib/lean/Init/Control/Lawful.ir
lib/lean/Init/Control/Lawful.ir.sig

The first 100 are listed.

distinfo 3

File

Size

SHA256

leanprover-lean4-v4.35.0_GH0.tar.gz

9.0233735e+07

6747b099d03d3675f2716e7cf5924a16bfbf75822b13a3d36f51f933ffcc307b

microsoft-mimalloc-v3.4.5_GH0.tar.gz

1.423876e+06

19a43af0645c57d348e729d5b31e23e912582911bb1047f795790834d3416221

Kha-lean4lean-lean4-bundle-4.35_GH0.tar.gz

444970

8e0b486737e8b812753317bc504e6e3afc3716398b0a2c19516a1143177291a9

Commit history 10

Date Commit Credits Log message

2026-10-13 9bcf1534aa Yuri Victorovich math/lean4: update 4.34.1 → 4.35.0

2026-09-25 007512b84e Yuri Victorovich math/lean4: update 4.34.0 → 4.34.1

2026-09-14 e55bf905b6 Yuri Victorovich math/lean4: update 4.33.1 → 4.34.0

2026-09-14

abf08b8dfe

Yuri Victorovich

math/lean4: broken on 14

Reported by: fallout

2026-09-05 6dd0fb54cd Yuri Victorovich math/lean4: update 4.32.1 → 4.33.1

The latest 5 of 10 in the history this site was built from.