leanprover/lean4

Las issues en las que quizá ya trabaja alguien aparecen al final. Ordenar todo por fecha

• `WPMonad.withFrameClosure` restricted to `m : Type → Type` and `R : Type`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 3/5 1-2 días Aptitud para principiantes 67/100

  leanprover/lean4#15424 · Abierto el 1/10/2026

  Los mantenedores suelen responder en 1 día

• Wrong `SymM` maximal sharing behavior for `letE`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100

  leanprover/lean4#15423 · Abierto el 1/10/2026

  Los mantenedores suelen responder en 1 día

• module system: `addDecl` accepts public declarations whose exported type mentions private constants

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 55/100

  leanprover/lean4#15401 · 1 comentario · Abierto el 29/9/2026

  Los mantenedores suelen responder en 1 día

• module system: `by` blocks in `variable` binders inside `public section` put unexported aux proofs into public signatures

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 45/100

  leanprover/lean4#15393 · 1 comentario · Abierto el 28/9/2026

  Los mantenedores suelen responder en 1 día

• first `grind +suggestions` / `try?` takes minutes with `import Mathlib` since v4.35.0-rc2 (#15159)

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

  leanprover/lean4#15392 · 2 reacciones · Abierto el 28/9/2026

  Los mantenedores suelen responder en 1 día

• `bv_decide` no longer reifies a `BitVec` atom reached through a `@[reducible]` accessor over a structure field whose width is computed by a `def` (regression in v4.34.0)

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 56/100

  leanprover/lean4#15368 · Abierto el 27/9/2026

  Los mantenedores suelen responder en 1 día

• Compiler PANIC in `ExplicitBoxing` when an auto-generated `SizeOf` instance reaches codegen (regression since 4.28)

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 4/5 3-5 días Aptitud para principiantes 70/100

  leanprover/lean4#15346 · 1 comentario · 1 reacción · Abierto el 26/9/2026

  Los mantenedores suelen responder en 1 día

• `getMainModule` breaks when accessing files through URIs with `#`-fragments

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 4/5 3-5 días Aptitud para principiantes 58/100

  leanprover/lean4#15342 · Abierto el 26/9/2026

  Los mantenedores suelen responder en 1 día

• The test lake/tests/cacheTransfer fails

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100

  leanprover/lean4#15335 · 1 comentario · Abierto el 25/9/2026

  Los mantenedores suelen responder en 1 día

• Tests don't respect the CTEST_PARALLEL_LEVEL environment variable

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 3/5 1-2 días Aptitud para principiantes 55/100

  leanprover/lean4#15334 · Abierto el 25/9/2026

  Los mantenedores suelen responder en 1 día

• Missed specialization leading to bad code

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug code-generator

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  leanprover/lean4#15328 · Abierto el 25/9/2026

  Los mantenedores suelen responder en 1 día

• Inconsistency in functions handling private names

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 3/5 1-2 días Aptitud para principiantes 65/100

  leanprover/lean4#15308 · Abierto el 24/9/2026

  Los mantenedores suelen responder en 1 día

• Anonymous instances are sometimes silently not created

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  leanprover/lean4#15302 · Abierto el 24/9/2026

  Los mantenedores suelen responder en 1 día

• Type ascription with autoParam under ∀ᵐ times out

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 4/5 3-5 días Aptitud para principiantes 40/100

  leanprover/lean4#15284 · 1 comentario · Abierto el 23/9/2026

  Los mantenedores suelen responder en 1 día

• feat: a way to build a project inside `lake check`'s sandbox without checking it

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 3/5 1-2 días Aptitud para principiantes 55/100

  leanprover/lean4#15282 · 1 comentario · 1 reacción · Abierto el 23/9/2026

  Los mantenedores suelen responder en 1 día

• feat: `lake check --allow-sorry`, to permit `sorryAx` in in-progress projects

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 3/5 1-2 días Aptitud para principiantes 65/100

  leanprover/lean4#15281 · Abierto el 23/9/2026

  Los mantenedores suelen responder en 1 día

• grind with BitVec.allOnes is broken by replacing variable with literal constant

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

  leanprover/lean4#15261 · 2 comentarios · Abierto el 22/9/2026

  Los mantenedores suelen responder en 1 día

• grind_hom does not recognize arithmetic properties of constant bitmasks

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 50/100

  leanprover/lean4#15260 · 3 reacciones · Abierto el 21/9/2026

  Los mantenedores suelen responder en 1 día

• Std.Http.URI query encoding changes literal plus signs to spaces

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-medium

  Dificultad 3/5 1-2 días Aptitud para principiantes 68/100

  leanprover/lean4#15246 · Abierto el 21/9/2026

  Los mantenedores suelen responder en 1 día

• RFC: safe withExclusive wrapper around isExclusiveUnsafe

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  RFC

  Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

  leanprover/lean4#15235 · Abierto el 20/9/2026

  Los mantenedores suelen responder en 1 día

• `#print axioms` / `collectAxioms` under-reports axioms of imported inductives (in-progress sentinel cached by `exportedAxiomsExt`)

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  leanprover/lean4#15226 · 2 comentarios · 1 reacción · Abierto el 19/9/2026

  Los mantenedores suelen responder en 1 día

• `@[deprecated]` on a structure field projection does not warn when constructing the field

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  leanprover/lean4#15203 · Abierto el 17/9/2026

  Los mantenedores suelen responder en 1 día

• `simpDiscrCtor?` is broken in the presence of non-type parameters

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug code-generator P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  leanprover/lean4#15200 · Abierto el 17/9/2026

  Los mantenedores suelen responder en 1 día

• `#guard_msgs` hides error messages from commands outside of it

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-low

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  leanprover/lean4#15196 · Abierto el 17/9/2026

  Los mantenedores suelen responder en 1 día

• `Nat.shiftLeft` by 2^32 or more crashes Lean in `rfl`, `decide`, `simp`, `cbv`, `grind` and the compiler

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  leanprover/lean4#15193 · 1 reacción · Abierto el 17/9/2026

  Los mantenedores suelen responder en 1 día

• grind explodes on a simple example with `Array.range`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

  leanprover/lean4#15183 · 1 comentario · Abierto el 16/9/2026

  Los mantenedores suelen responder en 1 día

• MULTI_THREAD=OFF build fails: std::adopt_lock_t used in thread.h without including <mutex>

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-low

  Dificultad 2/5 1-3 horas Aptitud para principiantes 86/100

  leanprover/lean4#15172 · 1 comentario · Abierto el 15/9/2026

  Los mantenedores suelen responder en 1 día

• perf: reduce Nat.powMod kernel replay cost

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

  leanprover/lean4#15166 · Abierto el 15/9/2026

  Los mantenedores suelen responder en 1 día

• RFC: structured log entries in Lake, and a JSON log format for `lake build`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-high RFC

  Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

  leanprover/lean4#15139 · 2 comentarios · Abierto el 12/9/2026

  Los mantenedores suelen responder en 1 día

• RFC: Support dependency in Verso docstrings

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-medium RFC

  Dificultad 5/5 Más de una semana Aptitud para principiantes 45/100

  leanprover/lean4#15137 · 2 reacciones · Abierto el 11/9/2026

  Los mantenedores suelen responder en 1 día

• custom semantic highlighting appears only when source file is first edited

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

  leanprover/lean4#15118 · 6 comentarios · Abierto el 11/9/2026

  Los mantenedores suelen responder en 1 día

• Linux: libleanshared.so exports a partial _Unwind_* ABI, breaking C++ exceptions inside FFI libraries built against libstdc++

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  leanprover/lean4#15112 · 1 comentario · 1 reacción · Abierto el 10/9/2026

  Los mantenedores suelen responder en 1 día

• Missing goal state after `grind =>`, `sym =>` and `impossible by`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 3/5 1-2 días Aptitud para principiantes 70/100

  leanprover/lean4#15108 · 1 comentario · 2 reacciones · Abierto el 10/9/2026

  Los mantenedores suelen responder en 1 día

• `grind` failing to apply lemma if instance is not syntactically equal

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 55/100

  leanprover/lean4#15082 · 1 comentario · Abierto el 9/9/2026

  Los mantenedores suelen responder en 1 día

• RFC: use `Std.Refl`/`Std.Symm` instances in `rfl`/`symm`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-medium RFC

  Dificultad 5/5 Más de una semana Aptitud para principiantes 39/100

  leanprover/lean4#15081 · 2 reacciones · Abierto el 9/9/2026

  Los mantenedores suelen responder en 1 día

• `deriving instance CoeFun/CoeSort` generates opaque aux constant for reducible type synonyms

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 55/100

  leanprover/lean4#15065 · 1 comentario · 3 reacciones · Abierto el 8/9/2026

  Los mantenedores suelen responder en 1 día

• Std.Http minor cleanups

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  RFC

  Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

  leanprover/lean4#15051 · 1 reacción · Abierto el 7/9/2026

  Los mantenedores suelen responder en 1 día

• No `goalsAccomplished` message is produced for theorems generated using `elab`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 3/5 1-2 días Aptitud para principiantes 72/100

  leanprover/lean4#15044 · 1 comentario · Abierto el 6/9/2026

  Los mantenedores suelen responder en 1 día

• Delaborator omits an instance binder's name when it is used only in a later binder's type

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-medium

  Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100

  leanprover/lean4#15037 · Abierto el 4/9/2026

  Los mantenedores suelen responder en 1 día

• `pp.all` output does not round-trip when a local's type has `optParam`/`autoParam` binders

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-low

  Dificultad 4/5 3-5 días Aptitud para principiantes 55/100

  leanprover/lean4#15035 · Abierto el 4/9/2026

  Los mantenedores suelen responder en 1 día

• `Failed to find LCNF signature` reported to users where v4.20 gave the `noncomputable` hint

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-low

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  leanprover/lean4#15034 · Abierto el 4/9/2026

  Los mantenedores suelen responder en 1 día

• Compiler PANIC in `ExplicitBoxing` when `deriving Repr`/`BEq` over an `unsafe instance`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

  leanprover/lean4#15033 · 1 comentario · Abierto el 4/9/2026

  Los mantenedores suelen responder en 1 día

• `Nat.lt` docstring

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-low

  Dificultad 1/5 Menos de una hora Aptitud para principiantes 85/100

  leanprover/lean4#15014 · Abierto el 4/9/2026

  Los mantenedores suelen responder en 1 día

• Very high CPU usage when making any edits at the top of a file

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  leanprover/lean4#15013 · 4 comentarios · 4 reacciones · Abierto el 4/9/2026

  Los mantenedores suelen responder en 1 día

• typecheck error sometimes escapes `first`

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  leanprover/lean4#15000 · 1 reacción · Abierto el 2/9/2026

  Los mantenedores suelen responder en 1 día

• stack overflow hangs instead of aborting when the fault lands inside the allocator

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 25/100

  leanprover/lean4#14992 · Abierto el 1/9/2026

  Los mantenedores suelen responder en 1 día

• olean loader: no-mmap fallback re-reads the entire file after the header probe

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-low

  Dificultad 3/5 1-2 días Aptitud para principiantes 72/100

  leanprover/lean4#14991 · Abierto el 1/9/2026

  Los mantenedores suelen responder en 1 día

• Private proof materializes a public equation theorem

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-medium

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  leanprover/lean4#14986 · Abierto el 1/9/2026

  Los mantenedores suelen responder en 1 día

• `subst` and `simp` reorder hypotheses when rewriting

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug P-low

  Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

  leanprover/lean4#14985 · 1 reacción · Abierto el 1/9/2026

  Los mantenedores suelen responder en 1 día

• Meta issue: Lean Kernel Logic renovation

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  P-high

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  leanprover/lean4#14977 · 1 comentario · 9 reacciones · Abierto el 31/8/2026

  Los mantenedores suelen responder en 1 día