python-to-lean4-translator
Translates Python into Lean 4 for interactive theorem proving, handling dynamic types and duck typing by specializing to the concrete types actually used. Use when proving correctness of a Python algorithm beyond what testing can establish, or when building a verified reference for numerical or combinatorial Python code.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill python-to-lean4-translator100
Quality
100%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
Discovery
100%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is an excellent skill description that clearly articulates a specialized capability (Python to Lean 4 translation for formal verification), includes natural trigger terms users would employ, and explicitly states both what the skill does and when to use it. The description is concise yet comprehensive, targeting a distinct niche that minimizes conflict risk with other skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists specific concrete actions: 'Translates Python into Lean 4', 'handling dynamic types and duck typing', 'specializing to concrete types', 'proving correctness', 'building a verified reference'. Multiple distinct capabilities are clearly articulated. | 3 / 3 |
Completeness | Clearly answers both what ('Translates Python into Lean 4 for interactive theorem proving, handling dynamic types...') and when ('Use when proving correctness of a Python algorithm beyond what testing can establish, or when building a verified reference...'). | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'Python', 'Lean 4', 'theorem proving', 'proving correctness', 'verified', 'numerical', 'combinatorial', 'algorithm'. Good coverage of domain-specific terms a user seeking this functionality would use. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche combining Python-to-Lean translation with formal verification. The specific language pair (Python to Lean 4) and use case (theorem proving, verified reference) make conflicts with other skills very unlikely. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
100%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is an excellent skill that demonstrates mastery of concise technical writing. It efficiently maps Python constructs to Lean 4 equivalents, provides a complete worked example with proof strategy, and clearly articulates what to skip and what pitfalls to avoid. The delta-based structure and type-narrowing workflow show sophisticated understanding of the translation problem.
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | Extremely lean and efficient. Uses tables for mappings, avoids explaining what Python or Lean are, assumes Claude knows both languages. Every section adds novel, non-obvious translation guidance. | 3 / 3 |
Actionability | Provides concrete, executable Lean code examples with complete syntax. The worked example shows both spec and algorithm versions with a proof skeleton. The type mapping table gives direct, copy-paste-ready translations. | 3 / 3 |
Workflow Clarity | Clear workflow: narrow types first, translate twice (spec + algorithm), prove equivalence. The type-narrowing step is explicitly sequenced (1-2-3). The 'Do not' section provides validation guardrails against common mistakes. | 3 / 3 |
Progressive Disclosure | Appropriately structured as a delta over another skill file, with clear reference. Content is well-organized into logical sections (mappings, narrowing, example, skip list, do-nots, output format) without being monolithic or requiring deep navigation. | 3 / 3 |
Total | 12 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Reviewed
Table of Contents
Is this your skill?
If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.