commit: 6b12e4b969dd147fe7d9df02619e4f4f0c001700

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Thu Aug 20 00:29:31 2026 +0200
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Aug 20 00:29:31 2026 +0200
tree: 497b2f70dfc4c161d5ff0830b02bccdf296c0968
parent: 01fe11016b49e852a896f62b1590f1a763c7b145 [diff]

test: for `is_prop` bug in kernel

This PR adds another test for the `is_prop` bug in the kernel.
The exploit was submitted by Daniel Selsam (OpenAI) and was generated using OpenAI's internal models.

tests/elab/kernel_is_prop_issue.lean[Added - diff]

1 file changed

tree: 497b2f70dfc4c161d5ff0830b02bccdf296c0968

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.