diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 2431721f6b2f..3402b4d2f4a8 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,115 +1,115 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.32.0
+DISTVERSION=	4.32.1
 CATEGORIES=	math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment
 
 MAINTAINER=	yuri@FreeBSD.org
 COMMENT=	Theorem prover and functional language for math (new gen)
 WWW=		https://lean-lang.org/ \
 		https://github.com/leanprover/lean4
 
 LICENSE=	APACHE20
 LICENSE_FILE=	${WRKSRC}/LICENSE
 
 BROKEN_armv7=	compilation fails: ../../.build/stage1/lib/temp/Init/Coe.depend: No such file or directory
 BROKEN_i386=	linking fails: INTERNAL PANIC: out of memory (during: Linking runLinter)
 
 BUILD_DEPENDS=	bash:shells/bash \
 		cadical:math/cadical \
 		gsed:textproc/gsed \
 		leantar:math/leangz
 LIB_DEPENDS=	libgmp.so:math/gmp \
 		libuv.so:devel/libuv
 RUN_DEPENDS=	cadical:math/cadical \
 		leantar:math/leangz
 TEST_DEPENDS=	gtail:sysutils/coreutils \
 		gsed:textproc/gsed
 
 USES=		cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # ninja fails + gmake scripts are included in the project
 
 USE_GITHUB=	yes
 GH_ACCOUNT=	leanprover
 
 CFLAGS+=	-fPIC
 CXXFLAGS+=	-fPIC
 
 CMAKE_OFF=	USE_MIMALLOC \
 		INSTALL_LEANTAR
 
 #MAKE_ARGS+=	V=1 VERBOSE=1
 MAKE_ENV=	LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean
 
 BINARY_ALIAS=	make=${GMAKE} \
 		python=${PYTHON_CMD} \
 		sed=${LOCALBASE}/bin/gsed
 
 .include <bsd.port.pre.mk>
 
 CMAKE_ARGS+=	-DLEANTAR=${LOCALBASE}/bin/leantar
 
 post-configure:
 	# Copy leantar to build bin directories for tests (INSTALL_LEANTAR=OFF disables the built-in copy)
 	@${MKDIR} ${BUILD_WRKSRC}/stage0/bin ${BUILD_WRKSRC}/stage1/bin
 	@${CP} ${LOCALBASE}/bin/leantar ${BUILD_WRKSRC}/stage0/bin/
 	@${CP} ${LOCALBASE}/bin/leantar ${BUILD_WRKSRC}/stage1/bin/
 
 # fails to build on 14 w/out this:
 .if ${OSREL:R} <= 14
 BINARY_ALIAS+=	ar=llvm-ar
 .endif
 
 pre-everything::
 	@${ECHO_MSG} ""
 	@${ECHO_MSG} "Please note that build Lean requires /proc to be mounted."
 	@${ECHO_MSG} ""
 	@${ECHO_MSG} "  The usual way to do this is to add this line to /etc/fstab:"
 	@${ECHO_MSG} "  proc /proc procfs rw 0 0"
 	@${ECHO_MSG} ""
 	@${ECHO_MSG} "  and then run this command as root:"
 	@${ECHO_MSG} "  # mount /proc"
 	@${ECHO_MSG} ""
 
 post-patch:
 	# Add weakLeancArgs = ["-fPIC"] to all test lakefile.toml files
 	# Skip inputFile test: its translate-config test expects exact TOML-to-Lean output
 	@${FIND} ${WRKSRC}/tests -name "lakefile.toml" -not -path "*/inputFile/*" | while read f; do \
 		${GREP} -q "weakLeancArgs" "$$f" || \
 		( ${PRINTF} 'weakLeancArgs = ["-fPIC"]\n\n' | ${CAT} - "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f" ); \
 	done
 	# Add weakLeancArgs to lakefile.lean files that define packages
 	@${FIND} ${WRKSRC}/tests -name "lakefile.lean" | while read f; do \
 		if ${GREP} -q "^package .* where" "$$f" && ! ${GREP} -q "weakLeancArgs" "$$f"; then \
 			${AWK} '/^package .* where$$/ {print; print "  weakLeancArgs := #[\"-fPIC\"]"; next} 1' "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f"; \
 		fi; \
 	done
 
 post-install:
 	# remove empty dirs
 	@${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete
 	# remove stray files
 	@${RM} ${STAGEDIR}${PREFIX}/LICENSE*
 	# remove bin/cadical, workaround for https://github.com/leanprover/lean4/issues/5603
 	@${RM} ${STAGEDIR}${PREFIX}/bin/cadical
 	# remove bin/leantar (we use the one from math/leangz)
 	@${RM} ${STAGEDIR}${PREFIX}/bin/leantar
 	# strip binaries
 	@cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \
 		bin/lake \
 		bin/lean \
 		bin/leanc \
 		bin/leanir \
 		lib/lean/libInit_shared.so \
 		lib/lean/libleanshared.so \
 		lib/lean/libleanshared_1.so \
 		lib/lean/libleanshared_2.so \
 		lib/lean/libLake_shared.so
 
 # tests as of 4.25.2-20251201: 100% tests passed, 0 tests failed out of 3367
 # tests as of 4.29.0-rc2: 99% tests passed, 12 tests failed out of 3584, see https://github.com/leanprover/lean4/issues/12721
 # tests as of 4.29.0: 99% tests passed, 18 tests failed out of 3582, see https://github.com/leanprover/lean4/issues/13174
 # tests as of 4.29.1: 99% tests passed, 24 tests failed out of 3584
 # tests as of 4.30.0: 100% tests passed, 0 tests failed out of 3678
 # tests as of 4.31.0: 99% tests passed, 2 tests failed out of 3858
 # 2 failures are not port issues: cache/test.sh, ltar/test.sh: leantar panic (math/leangz bug, see reproducer-leangz/)
 
 .include <bsd.port.post.mk>
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index 2af2d958e506..f98762b632d4 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1784011437
-SHA256 (leanprover-lean4-v4.32.0_GH0.tar.gz) = f39c6d87a9b4e9253bef15ffae460d2652b668e619688e4c01e59bbd2cd3b002
-SIZE (leanprover-lean4-v4.32.0_GH0.tar.gz) = 75094778
+TIMESTAMP = 1785103908
+SHA256 (leanprover-lean4-v4.32.1_GH0.tar.gz) = 5ee893d6081dba103c3d1206930a0637f9dd8afe3c631823b98a21593386dbd7
+SIZE (leanprover-lean4-v4.32.1_GH0.tar.gz) = 75094335
diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt
index 5f9d89f2d38f..8098ed7948d6 100644
--- a/math/lean4/files/patch-src_CMakeLists.txt
+++ b/math/lean4/files/patch-src_CMakeLists.txt
@@ -1,59 +1,59 @@
---- src/CMakeLists.txt.orig	2026-06-13 21:32:55 UTC
+--- src/CMakeLists.txt.orig	2026-07-22 17:50:04 UTC
 +++ src/CMakeLists.txt
-@@ -395,7 +395,7 @@ endif()
+@@ -407,7 +407,7 @@ endif()
    endif()
  endif()
  
 -include_directories(${CMAKE_BINARY_DIR}/include)
 +include_directories(BEFORE ${CMAKE_BINARY_DIR}/include)
  
  # Pick up `llvm-config` to setup LLVM flags.
  if(LLVM)
-@@ -537,7 +537,7 @@ endif()
+@@ -549,7 +549,7 @@ endif()
    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm")
  endif()
  
 -if(CMAKE_SYSTEM_NAME MATCHES "Linux")
 +if(CMAKE_SYSTEM_NAME MATCHES "Linux|FreeBSD")
    if(BSYMBOLIC)
      string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
      string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
-@@ -550,6 +550,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
+@@ -562,6 +562,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
      " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
    )
    string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
 +elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD")
 +  if(BSYMBOLIC)
 +    string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
 +    string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
 +  endif()
 +  string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
 +  string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
 +  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
 +  string(
 +    APPEND LAKESHARED_LINKER_FLAGS
 +    " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
 +  )
 +  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
  elseif(CMAKE_SYSTEM_NAME MATCHES "Darwin")
    string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
    string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
-@@ -708,6 +721,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
+@@ -720,6 +733,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
  # Lean code only needs this one include
  string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include")
  
 +# Include extra flags (e.g., -fPIC on FreeBSD)
 +string(APPEND LEANC_OPTS " ${LEANC_EXTRA_FLAGS}")
 +
  # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc`
  string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
  string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
-@@ -1025,7 +1041,7 @@ install(
+@@ -1037,7 +1053,7 @@ install(
  
  install(
    DIRECTORY "${CMAKE_SOURCE_DIR}/"
 -  DESTINATION src/lean
 +  DESTINATION share/lean4/src/lean
    FILES_MATCHING
    PATTERN "*.lean"
    PATTERN "*.md"
diff --git a/math/lean4/files/patch-src_include_lean_lean.h b/math/lean4/files/patch-src_include_lean_lean.h
new file mode 100644
index 000000000000..85a25f0ea4ad
--- /dev/null
+++ b/math/lean4/files/patch-src_include_lean_lean.h
@@ -0,0 +1,29 @@
+--- src/include/lean/lean.h.orig	2026-07-22 17:50:04 UTC
++++ src/include/lean/lean.h
+@@ -17,6 +17,10 @@ Author: Leonardo de Moura
+ #include <lean/mimalloc.h>
+ #endif
+ 
++#if defined(__FreeBSD__)
++#include <sys/param.h>
++#endif
++
+ #ifdef __cplusplus
+ #include <atomic>
+ #include <stdlib.h>
+@@ -484,7 +488,15 @@ __attribute__((nothrow))
+ // `__attribute__((nothrow))` to be present or `noexcept`.
+ __attribute__((nothrow))
+ #endif
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1500000
+ void free_sized(void* ptr, size_t);
++#else
++#  ifdef __cplusplus
++void free_sized(void* ptr, size_t) throw();
++#  else
++void free_sized(void* ptr, size_t);
++#  endif
++#endif
+ #endif
+ 
+ static inline void lean_free_small_object(lean_object * o) {
diff --git a/math/lean4/files/patch-src_runtime_object.cpp b/math/lean4/files/patch-src_runtime_object.cpp
index c8a62465f1d7..df8a2d96b019 100644
--- a/math/lean4/files/patch-src_runtime_object.cpp
+++ b/math/lean4/files/patch-src_runtime_object.cpp
@@ -1,25 +1,25 @@
 -- fix breakage caused by strict matching of the throw() attribute in FreeBSD 16.0
 
 --- src/runtime/object.cpp.orig	2026-06-21 11:16:11 UTC
 +++ src/runtime/object.cpp
 @@ -22,6 +22,8 @@ Author: Leonardo de Moura
  #include "runtime/io.h"
  #include "runtime/hash.h"
  
 +#include <sys/param.h>
 +
  #if defined(__GLIBC__) || defined(__APPLE__)
      #define LEAN_SUPPORTS_BACKTRACE 1
  #else
 @@ -61,7 +63,11 @@ __attribute__((nothrow))
  // `__attribute__((nothrow))` to be present or `noexcept`.
  __attribute__((nothrow))
  #endif
-+#if !defined(__FreeBSD__) || __FreeBSD_version < 1600000
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1500000
  __attribute__((weak)) void free_sized(void *ptr, size_t) {
 +#else
 +__attribute__((weak)) void free_sized(void *ptr, size_t) throw() {
 +#endif
      free(ptr);
  }
  #endif
diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt
index 403d15edeaac..1b499230c8d4 100644
--- a/math/lean4/files/patch-stage0_src_CMakeLists.txt
+++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt
@@ -1,59 +1,59 @@
---- stage0/src/CMakeLists.txt.orig	2026-06-13 21:32:55 UTC
+--- stage0/src/CMakeLists.txt.orig	2026-07-22 17:50:04 UTC
 +++ stage0/src/CMakeLists.txt
-@@ -395,7 +395,7 @@ endif()
+@@ -407,7 +407,7 @@ endif()
    endif()
  endif()
  
 -include_directories(${CMAKE_BINARY_DIR}/include)
 +include_directories(BEFORE ${CMAKE_BINARY_DIR}/include)
  
  # Pick up `llvm-config` to setup LLVM flags.
  if(LLVM)
-@@ -537,7 +537,7 @@ endif()
+@@ -549,7 +549,7 @@ endif()
    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm")
  endif()
  
 -if(CMAKE_SYSTEM_NAME MATCHES "Linux")
 +if(CMAKE_SYSTEM_NAME MATCHES "Linux|FreeBSD")
    if(BSYMBOLIC)
      string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
      string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
-@@ -550,6 +550,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
+@@ -562,6 +562,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
      " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
    )
    string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
 +elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD")
 +  if(BSYMBOLIC)
 +    string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
 +    string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
 +  endif()
 +  string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
 +  string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
 +  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
 +  string(
 +    APPEND LAKESHARED_LINKER_FLAGS
 +    " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
 +  )
 +  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
  elseif(CMAKE_SYSTEM_NAME MATCHES "Darwin")
    string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
    string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
-@@ -708,6 +721,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
+@@ -720,6 +733,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
  # Lean code only needs this one include
  string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include")
  
 +# Include extra flags (e.g., -fPIC on FreeBSD)
 +string(APPEND LEANC_OPTS " ${LEANC_EXTRA_FLAGS}")
 +
  # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc`
  string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
  string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
-@@ -1025,7 +1041,7 @@ install(
+@@ -1037,7 +1053,7 @@ install(
  
  install(
    DIRECTORY "${CMAKE_SOURCE_DIR}/"
 -  DESTINATION src/lean
 +  DESTINATION share/lean4/src/lean
    FILES_MATCHING
    PATTERN "*.lean"
    PATTERN "*.md"
diff --git a/math/lean4/files/patch-stage0_src_include_lean_lean.h b/math/lean4/files/patch-stage0_src_include_lean_lean.h
new file mode 100644
index 000000000000..412f1f76568e
--- /dev/null
+++ b/math/lean4/files/patch-stage0_src_include_lean_lean.h
@@ -0,0 +1,29 @@
+--- stage0/src/include/lean/lean.h.orig	2026-07-22 17:50:04 UTC
++++ stage0/src/include/lean/lean.h
+@@ -17,6 +17,10 @@ Author: Leonardo de Moura
+ #include <lean/mimalloc.h>
+ #endif
+ 
++#if defined(__FreeBSD__)
++#include <sys/param.h>
++#endif
++
+ #ifdef __cplusplus
+ #include <atomic>
+ #include <stdlib.h>
+@@ -484,7 +488,15 @@ __attribute__((nothrow))
+ // `__attribute__((nothrow))` to be present or `noexcept`.
+ __attribute__((nothrow))
+ #endif
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1500000
+ void free_sized(void* ptr, size_t);
++#else
++#  ifdef __cplusplus
++void free_sized(void* ptr, size_t) throw();
++#  else
++void free_sized(void* ptr, size_t);
++#  endif
++#endif
+ #endif
+ 
+ static inline void lean_free_small_object(lean_object * o) {
diff --git a/math/lean4/files/patch-stage0_src_runtime_object.cpp b/math/lean4/files/patch-stage0_src_runtime_object.cpp
index ca40a370d5be..98de136bdefb 100644
--- a/math/lean4/files/patch-stage0_src_runtime_object.cpp
+++ b/math/lean4/files/patch-stage0_src_runtime_object.cpp
@@ -1,25 +1,25 @@
 -- fix breakage caused by strict matching of the throw() attribute in FreeBSD 16.0
 
 --- stage0/src/runtime/object.cpp.orig	2026-06-21 11:16:11 UTC
 +++ stage0/src/runtime/object.cpp
 @@ -22,6 +22,8 @@ Author: Leonardo de Moura
  #include "runtime/io.h"
  #include "runtime/hash.h"
  
 +#include <sys/param.h>
 +
  #if defined(__GLIBC__) || defined(__APPLE__)
      #define LEAN_SUPPORTS_BACKTRACE 1
  #else
 @@ -61,7 +63,11 @@ __attribute__((nothrow))
  // `__attribute__((nothrow))` to be present or `noexcept`.
  __attribute__((nothrow))
  #endif
-+#if !defined(__FreeBSD__) || __FreeBSD_version < 1600000
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1500000
  __attribute__((weak)) void free_sized(void *ptr, size_t) {
 +#else
 +__attribute__((weak)) void free_sized(void *ptr, size_t) throw() {
 +#endif
      free(ptr);
  }
  #endif