Bootstrap Exchequer research environment and native Android console

[jain-Igtm]

What changed

• initialized Exchequer as a general Lean 4 + Mathlib research repository
• added CI that rejects sorry and admit and kernel-checks all imported Lean sources
• separated formal proofs from informal research notes
• added the first machine-checked Erdős–Straus definitions and lemmas as an initial specimen
• added a fully native Kotlin and Jetpack Compose Android client
• added a compact repository feed for verified declarations, recorded obstructions, and written mathematics
• made the Android client load feed data only from the exact commit SHA of a successful Lean workflow run
• added Android CI that builds and uploads a debug APK

Android interface

The app contains no WebView and no remotely downloaded UI. It displays only repository-derived information:

• latest Lean build result, commit, and completion time
• verified declarations tied to the last successful Lean commit
• explicitly recorded obstructions
• recent commit activity
• a native collapsible Math / Lean source panel

Proof and repository data update over the network without reinstalling the APK. An APK update is needed only when native application code changes.

Validation

• Lean verification workflow
• Android debug APK workflow using JDK 17, Gradle 9.6.1, AGP 9.3.1, Kotlin 2.4.10, and Compose BOM 2026.06.00

Next steps

• merge after both Lean and Android checks pass
• expand the feed schema as additional general research problems are added