Lean Copilot Files

LLMs as Copilots for Theorem Proving in Lean

This is an exact mirror of the Lean Copilot project, hosted at https://github.com/lean-dojo/LeanCopilot. SourceForge is not affiliated with Lean Copilot. For more information, see the SourceForge Open Source Mirror Directory.

The interactive file manager requires Javascript. Please enable it or use sftp or scp.
You may still browse the files here.

Name	Modified	Size	InfoDownloads / Week
Parent folder
x86_64-linux.tar.gz	2025-08-14	108.2 MB	0
arm64-linux.tar.gz	2025-08-14	102.9 MB	0
arm64-macOS.tar.gz	2025-08-14	4.1 MB	0
README.md	2025-08-14	435 Bytes	0
v4.22.0 source code.tar.gz	2025-08-14	174.6 kB	0
v4.22.0 source code.zip	2025-08-14	194.3 kB	0
Totals: 6 Items		215.6 MB	0

What's Changed

Bump to latest stable version Lean v4.23.0-rc1 (~ v4.22.0) by @Peiyang-Song in https://github.com/lean-dojo/LeanCopilot/pull/181

Note: this tag actually uses Lean v4.23.0-rc1, which is published almost at the same time as Lean v4.22.0, and thus our dependencies all got bumped to v4.23.0-rc1 directly and skipped v4.22.0.

Full Changelog: https://github.com/lean-dojo/LeanCopilot/compare/v4.21.0...v4.22.0

Source: README.md, updated 2025-08-14

Other Useful Business Software

Zenflow- The AI Workflow Engine for Software Devs

Parallel agents. Multi-agent orchestration. Specs that turn into shipped code. Zenflow automates planning, coding, testing, and verification.

Zenflow is the AI workflow engine built for real teams. Parallel agents plan, code, test, and verify in one workflow. With spec-driven development and deep context, Zenflow turns requirements into production-ready output so teams ship faster and stay in flow.

Try free now

MongoDB Atlas runs apps anywhere

Deploy in 115+ regions with the modern database for every enterprise.

MongoDB Atlas gives you the freedom to build and run modern applications anywhere—across AWS, Azure, and Google Cloud. With global availability in over 115 regions, Atlas lets you deploy close to your users, meet compliance needs, and scale with confidence across any geography.

Start Free

Recommended Projects

DeepSeek Prover V2
Advancing Formal Mathematical Reasoning via Reinforcement Learning
OpenLLM
Operating LLMs in production
LMDeploy
LMDeploy is a toolkit for compressing, deploying, and serving LLMs
GPT4All
Run Local LLMs on Any Device. Open-source
DeepSeekMath-V2
Towards self-verifiable mathematical reasoning

Lean Copilot Files

LLMs as Copilots for Theorem Proving in Lean

Get an email when there's a new version of Lean Copilot

What's Changed