diff --git a/metadata/md5-cache/sci-mathematics/lean-4.25.2 b/metadata/md5-cache/sci-mathematics/lean-4.25.2
deleted file mode 100644
index dd4714a..0000000
--- a/metadata/md5-cache/sci-mathematics/lean-4.25.2
+++ /dev/null
@@ -1,15 +0,0 @@
-BDEPEND=|| ( dev-lang/python:3.14 dev-lang/python:3.13 dev-lang/python:3.12 ) dev-build/make >=dev-build/cmake-3.28.5
-DEFINED_PHASES=compile configure install prepare pretend setup test
-DEPEND=dev-libs/gmp:= dev-libs/libuv:= sci-mathematics/cadical
-DESCRIPTION=The Lean Theorem Prover
-EAPI=8
-HOMEPAGE=https://leanprover-community.github.io/ https://github.com/leanprover/lean4/
-INHERIT=check-reqs cmake flag-o-matic python-any-r1
-IUSE=debug source
-KEYWORDS=~amd64
-LICENSE=Apache-2.0
-RDEPEND=dev-libs/gmp:= dev-libs/libuv:= sci-mathematics/cadical
-SLOT=0/4
-SRC_URI=https://github.com/leanprover/lean4/archive/refs/tags/v4.25.2.tar.gz -> lean-4.25.2.tar.gz
-_eclasses_=check-reqs	2a9731073c152554078a9a8df8fc0f1b	toolchain-funcs	98d9f464d912ae6b7316fb8a3721f5db	flag-o-matic	a7afe42e95fb46ce9691605acfb24672	multiprocessing	1e32df7deee68372153dca65f4a7c21f	ninja-utils	3a59a39e97af0f7c03f49cf3c22f262b	xdg-utils	42869b3c8d86a70ef3cf75165a395e09	cmake	a36a2a340635cb293524229ee6d2ef7a	python-utils-r1	dbb8c4d794033ad7e7221eaf567a6c90	python-any-r1	891415dfe39ad9b41b461f2b86354af0
-_md5_=48760dee67524d93db9a50cffcacb957
diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
deleted file mode 100644
index 6f0dd21..0000000
--- a/sci-mathematics/lean/Manifest
+++ /dev/null
@@ -1,3 +0,0 @@
-DIST lean-4.25.2.tar.gz 50069767 BLAKE2B ebf5b578cf5956a196049e3cde2c52f3dcc6b18078e556e096b3f47c399f4fef629eaa245716b795ad88f981fcc7dc3573e5a973a1c558e13d7c56fda206275b SHA512 cb9d43814a2e7ae8a33aed6fcaf8e64d834905c43846d310a74b1ed3215b20aa0585631a5e9e39df4c499b5de355b644f706e740e8a02572faf1626f1510c08b
-EBUILD lean-4.25.2.ebuild 1843 BLAKE2B 5e4da67180c9b7d801cbe490001316001d145a682852352f30c17a52f8e7ae3519c1958a99c1b2a19ab5f841827d73ee1753d75dc02cadde3cd2516941209007 SHA512 f37a1c87668396b8bfdd0c724e84dd26778f7a7ae26408265f3d3ebe8382e55876ff4248a9c912b68af05816704094f492f895d61a8e87ed4c094f87fc049a59
-MISC metadata.xml 954 BLAKE2B 338f64bbe848dca10f77fb7d5b7503684d36742139a4fd45f7a4c48250a11af6a78e40f5304d44166ce56f7fe4d22c6f980b55cab411bb7be93cc279694e9b66 SHA512 ec7c25a75237d2d54704e2d7b1811489a95780885c748a832643760d012eaceaeb5bfec9fc80509d5699940e749e770e841880cca1361848244b5031636e48b2
diff --git a/sci-mathematics/lean/lean-4.25.2.ebuild b/sci-mathematics/lean/lean-4.25.2.ebuild
deleted file mode 100644
index 96bbb51..0000000
--- a/sci-mathematics/lean/lean-4.25.2.ebuild
+++ /dev/null
@@ -1,103 +0,0 @@
-# Copyright 1999-2025 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-MAJOR="$(ver_cut 1)"
-
-CMAKE_MAKEFILE_GENERATOR="emake"
-PYTHON_COMPAT=( python3_{12..14} )
-
-inherit check-reqs cmake flag-o-matic python-any-r1
-
-DESCRIPTION="The Lean Theorem Prover"
-HOMEPAGE="https://leanprover-community.github.io/
-	https://github.com/leanprover/lean4/"
-
-if [[ "${PV}" == *9999* ]] ; then
-	inherit git-r3
-
-	EGIT_REPO_URI="https://github.com/leanprover/${PN}${MAJOR}"
-else
-	SRC_URI="https://github.com/leanprover/${PN}${MAJOR}/archive/refs/tags/v${PV/_/-}.tar.gz
-		-> ${P}.tar.gz"
-	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
-
-	KEYWORDS="~amd64"
-fi
-
-LICENSE="Apache-2.0"
-SLOT="0/${MAJOR}"
-IUSE="debug source"
-
-RDEPEND="
-	dev-libs/gmp:=
-	dev-libs/libuv:=
-	sci-mathematics/cadical
-"
-DEPEND="
-	${RDEPEND}
-"
-BDEPEND="
-	${PYTHON_DEPS}
-"
-
-CHECKREQS_DISK_BUILD="4G"
-CHECKREQS_DISK_USR="2G"
-
-# Built by lean's build tool.
-QA_FLAGS_IGNORED="
-usr/lib/lean/libInit_shared.so
-usr/lib/lean/libleanshared_1.so
-"
-
-pkg_setup() {
-	python-any-r1_pkg_setup
-}
-
-src_prepare() {
-	filter-lto
-
-	sed -e "s|-O[23]|${CFLAGS}|g" -i ./src/CMakeLists.txt || die
-
-	cmake_src_prepare
-}
-
-src_configure() {
-	local CMAKE_BUILD_TYPE=""
-
-	if use debug ; then
-		CMAKE_BUILD_TYPE="Debug"
-	else
-		CMAKE_BUILD_TYPE="Release"
-	fi
-
-	local -a mycmakeargs=(
-		-DCCACHE="OFF"
-		-DGIT_HASH="OFF"
-
-		-DUSE_MIMALLOC="OFF"
-		-DINSTALL_LICENSE="OFF"
-		-DINSTALL_CADICAL="OFF"
-
-		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
-		-DLEAN_EXTRA_LINKER_FLAGS="${LDFLAGS}"
-		-DLEAN_EXTRA_MAKE_OPTS="-s 262144"
-		-DLEANC_EXTRA_FLAGS="${CFLAGS}"
-	)
-	cmake_src_configure
-}
-
-src_compile() {
-	ulimit -s 30000000 || eerror "Failed to set required ulimit. Build may fail!"
-
-	cmake_src_compile
-}
-
-src_install() {
-	cmake_src_install
-
-	if ! use source ; then
-		rm -r "${ED}/usr/src" || die
-	fi
-}
diff --git a/sci-mathematics/lean/metadata.xml b/sci-mathematics/lean/metadata.xml
deleted file mode 100644
index c43ac3a..0000000
--- a/sci-mathematics/lean/metadata.xml
+++ /dev/null
@@ -1,22 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
-
-<pkgmetadata>
-  <maintainer type="project">
-    <email>sci-mathematics@gentoo.org</email>
-    <name>Gentoo Mathematics Project</name>
-  </maintainer>
-  <longdescription>
-    The Lean theorem prover is a proof assistant developed principally
-    by Leonardo de Moura at Microsoft Research.  Lean is a functional
-    programming language that makes it easy to write correct and
-    maintainable code. You can also use Lean as an interactive theorem
-    prover. Lean programming primarily involves defining types and
-    functions. This allows your focus to remain on the problem domain and
-    manipulating its data, rather than the details of programming.
-  </longdescription>
-  <upstream>
-    <bugs-to>https://github.com/leanprover/lean4/issues</bugs-to>
-    <remote-id type="github">leanprover/lean4</remote-id>
-  </upstream>
-</pkgmetadata>