python-to-lean4-translator
From the author
Translate Python programs to equivalent Lean4 code while preserving semantics and ensuring type safety. Use when users ask to convert, translate, or port Python code to Lean4, or when they need to verify Python algorithms using Lean4's theorem proving capabilities. Handles functions, classes, data structures, control flow, and ensures the generated Lean4 code is well-typed, executable, and can successfully run.
Install
npx skills add ArabelaTso/Skills-4-SE --skill python-to-lean4-translator -a claude-code
Installs to .claude/skills/python-to-lean4-translator/ · Each command fetches the skill straight from GitHub with the open skills CLI.
Byte-identical to the scanned commit, with the repository’s licence and a SOURCE.txt.
Want your agent to suggest skills while you type? See how to use skills from your IDE.
Safety checks on SKILL.md
No warnings.
Why 83
aiqbench computes the trust score from public signals. It is not a security audit, so read a skill before you install it.
Similar skills
Closest to this one by what they do and when they are used.
- c-cpp-to-lean4-translatorArabelaTso/Skills-4-SETranslate C or C++ programs into equivalent Lean4 code, preserving program semantics and ensuring the generated code is well-typed, executable, and can run successfully. Use when the user asks to convert C/C++ code to Lean4, port C/C++ programs to Lean4, translate imperative code to functional Lean4, or create Lean4 versions of C/C++ algorithms.Engineering★ 258
- python-to-dafny-translatorArabelaTso/Skills-4-SETranslate Python programs into equivalent Dafny code, preserving program semantics and ensuring the generated code is well-typed, executable, and verifiable. Use when the user asks to convert Python code to Dafny, port Python programs to Dafny, add formal verification to Python code, or create Dafny versions of Python algorithms with specifications.Engineering★ 258
- code-translationArabelaTso/Skills-4-SEConvert code between programming languages while preserving functionality and semantics. Use when: (1) Translating functions, classes, or modules between languages (Python, JavaScript/TypeScript, Java, Go, Rust, C/C++), (2) Migrating entire projects to a different language, (3) Need idiomatic translation that follows target language conventions, (4) Converting between different paradigms (OOP to functional, etc.), (5) Porting legacy code to modern languages. Provides language-specific patterns, idiomatic translation guides, and project migration strategies.Engineering★ 258
- writing-lean-proofstrailofbits/skillsWrites and reviews structured Lean 4 proofs and designs Lean libraries following Mathlib conventions. Use when proving theorems in Lean, formalizing mathematics or specifications in Lean 4, defining new types or definitions in a Lean library, reviewing Lean proofs for readability and maintainability, refactoring long tactic proofs into lemmas, filling in sorry placeholders in a Lean development, setting up CI or linters for a Lean project, diagnosing slow proofs or maxHeartbeats timeouts, or writing custom tactics, macros, or linters.Writing★ 7.8K
- developing-genkit-pythongoogle/skillsDevelop AI-powered applications using Genkit in Python. Use when the user asks about Genkit, AI agents, flows, or tools in Python, or when encountering Genkit errors, import issues, or API problems.OfficialEngineering★ 21.5K
- technical-analystjeremylongshore/tons-of-skills-marketplaceTechnical analysis translator for Product Managers. Use when the user needs to analyze a system, codebase, API, or technical concept in PM-friendly terms. Trigger with "understand system", "explain code", "technical analysis", "how does X work", or "what does this service do".Engineering★ 2.9K
Ratings & reviews
—
no reviews
Tried this skill? Rate it to help others. Sign in
Discussion
Join the discussion. Sign in