Lean IDE Guide
How to use the in-browser Lean 4 workspace for research derivation.
Using the Cloud Workspace
The in-browser Lean IDE provides a fully configured environment connected to the Krishnas Cloud Lean Service.
- Live Type-checking: LSP runs over WebSockets to provide immediate feedback.
- Infoview: View tactic state, goals, and diagnostics directly in the panel.
- Verification Run: Trigger a full sandboxed kernel verification to produce a VerificationRun certificate.