This Claude skill automates the scaffolding of Lean 4 projects, providing a standardized environment with pre-configured directory structures, Lake dependency management, and integrated testing frameworks. It streamlines the development workflow by ensuring best practices in naming conventions and documentation for libraries, applications, and formal verification projects.

When should I use new-project?

new-project is useful in the following scenarios: • Quickly initializing a new Lean 4 library with standardized GitHub-style dependencies and Lake configuration. • Setting up specialized Lean 4 projects for specific domains such as mathematics, web development, or graphics with the correct folder hierarchy. • Automating the creation of a robust testing suite using the Crucible framework to ensure code reliability from the start of a project. • Standardizing workspace documentation and metadata by automatically generating README.md and CLAUDE.md files tailored to Lean 4 development environments.

name	new-project
description	Scaffold a new Lean 4 project in the workspace. Use when creating a new project, library, or application.

New Project Scaffolding

Create a new Lean 4 project with the correct structure for this workspace.

Quick Start

Determine project category and name
Create directory structure
Generate lakefile.lean with GitHub-style dependencies
Create README.md and CLAUDE.md
Set up test structure with Crucible

Project Categories

Category	Purpose	Directory
graphics	TUI, GPU, widgets, rendering	`graphics/`
web	HTTP, HTML, templates	`web/`
network	HTTP client, protocols	`network/`
data	Databases, data structures	`data/`
apps	Applications	`apps/`
util	Utilities, tools	`util/`
math	Linear algebra, units	`math/`
audio	Sound synthesis	`audio/`
testing	Test frameworks	`testing/`

Directory Structure

<category>/<project>/
├── lakefile.lean
├── README.md
├── CLAUDE.md
├── <Project>/
│   └── Basic.lean
├── <Project>.lean
└── Tests/
    └── Main.lean

Template: lakefile.lean

import Lake
open Lake DSL

package «projectName» where
  leanOptions := #[
    ⟨`autoImplicit, false⟩
  ]

@[default_target]
lean_lib «ProjectName» where
  roots := #[`ProjectName]

require crucible from git "https://github.com/nathanial/crucible" @ "v0.0.1"

lean_exe tests where
  root := `Tests.Main

@[test_driver]
script test do
  let result ← IO.Process.run {
    cmd := ".lake/build/bin/tests"
    args := #[]
  }
  IO.println result
  return 0

Template: Main Library (.lean)

import ProjectName.Basic

Template: Basic.lean

namespace ProjectName

-- Your code here

end ProjectName

Template: Tests/Main.lean

import Crucible
import ProjectName

open Crucible

def main : IO Unit := Crucible.runTests "ProjectName" do
  describe "Basic" do
    it "works" do
      assert true

Template: CLAUDE.md

# <Project Name>

Brief description.

## Build

\`\`\`bash
lake build && lake test
\`\`\`

## Usage

\`\`\`lean
import ProjectName
\`\`\`

Naming Conventions

Directory: lowercase with hyphens (e.g., my-project)
Package: lowercase with hyphens in lakefile
Library/namespace: PascalCase (e.g., MyProject)
GitHub repo: matches directory name (except chronos → chronos-lean)

After Creation

lake build to verify structure
lake test to run initial tests
git init && git add -A && git commit -m "Initial commit"
Create GitHub repo and push
Add to workspace CLAUDE.md project list

new-project

When & Why to Use This Skill

Use Cases