diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 59197ac7f8b5..64de7b7817db 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,43 +1,42 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.5.0-rc1
-PORTREVISION=	2
+DISTVERSION=	4.5.0
 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/
 
 LICENSE=	APACHE20
 LICENSE_FILE=	${WRKSRC}/LICENSE
 
 BROKEN_i386=	linking fails: INTERNAL PANIC: out of memory (during: Linking runLinter)
 
 BUILD_DEPENDS=	bash:shells/bash
 LIB_DEPENDS=	libgmp.so:math/gmp
 
 USES=		cmake:noninja,testing compiler:c++14-lang gmake python:build # ninja fails + gmake scripts are included in the project
 
 USE_GITHUB=	yes
 GH_ACCOUNT=	leanprover
 
 CFLAGS+=	-fPIC
 CXXFLAGS+=	-fPIC
 
 BINARY_ALIAS=	make=${GMAKE} python=${PYTHON_CMD}
 
 post-install:
 	# remove empty dirs
 	@${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete
 	# remove stray files
 	@${RM} ${STAGEDIR}${PREFIX}/LICENSE*
 	# strip binaries
 	@cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \
 		bin/lake \
 		bin/lean \
 		bin/leanc \
 		lib/lean/libleanshared.so
 
 # 6 tests are known to fail due to bugs in the testcase code, see https://github.com/leanprover/lean4/issues/3179
 
 .include <bsd.port.mk>
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index d307f90be676..212153a2baf9 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1705134061
-SHA256 (leanprover-lean4-v4.5.0-rc1_GH0.tar.gz) = 8b5ae344816670adb2a68859b2f4c309592feb32674d477e46e061275f9e8129
-SIZE (leanprover-lean4-v4.5.0-rc1_GH0.tar.gz) = 17060956
+TIMESTAMP = 1706759565
+SHA256 (leanprover-lean4-v4.5.0_GH0.tar.gz) = 9a7e3661245cd6f115919695d7041396cf44b081b03421cac9bda6bf8353df0f
+SIZE (leanprover-lean4-v4.5.0_GH0.tar.gz) = 17060034