-
Notifications
You must be signed in to change notification settings - Fork 41
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
- Status: Open.#164 In cameronfreer/lean4-skills;
- Status: Open.#162 In cameronfreer/lean4-skills;
- Status: Open.#157 In cameronfreer/lean4-skills;
- Status: Open.#153 In cameronfreer/lean4-skills;
- Status: Open.#151 In cameronfreer/lean4-skills;
[Feature] Detect and guide the .of_eq fun _ ↦ rfl whnf-timeout when proving ComputableIn/Computable over heavy Primcodable encodings
enhancementNew feature or requestNew feature or requestStatus: Open.#150 In cameronfreer/lean4-skills;- Status: Open.#144 In cameronfreer/lean4-skills;
Used lean4-skills to complete a formal AI verification proof chain — interested in FORMA integration
Status: Open.#129 In cameronfreer/lean4-skills;docs: scope the docstring policy by workflow (proof-repair vs review vs new-file/new-decl)
enhancementNew feature or requestNew feature or requestStatus: Open.#116 In cameronfreer/lean4-skills;review: unify and expand review-hook-schema categories
enhancementNew feature or requestNew feature or requestStatus: Open.#115 In cameronfreer/lean4-skills;docs: add mathlib-review-taxonomy.md reference
enhancementNew feature or requestNew feature or requestStatus: Open.#114 In cameronfreer/lean4-skills;doctor: add module-system troubleshooting guidance
enhancementNew feature or requestNew feature or requestStatus: Open.#113 In cameronfreer/lean4-skills;