2026-10-14T12:55:02Z https://www.scidb.cn/oai

10.57760/sciencedb.011r9 2026-09-09T15:31:32Z

2026-09-09 GeoProofBench v0.1: a machine-checked proposition set for digital elevation model analysis doi:10.57760/sciencedb.011r9 en Digital elevation model (DEM) analysis underlies terrain-related work across geomorphology, hydrology, and civil engineering, yet published algorithms are rarely machine-checked. GeoProofBench (GPB) v0.1 is a proposition set of terrain-analysis claims expressed in Dafny and Lean 4, with a reproducible pipeline that compiles each proposition to a numerical witness, a Wolfram symbolic check, and a manim visualization, keyed to a GPB-N ENTRY: PASS verdict. This deposit contains six first-order operators, composition records (including fill-then-watershed), counter-example grids, five noise levels, four DEM stacks plus three public product windows (USGS 3DEP lidar, Alaska IFSAR, Copernicus GLO-30), Dafny/Lean sources, Python/Wolfram drivers, and mp4 animations. Data are licensed CC-BY-4.0; software is licensed MIT. Public file access is intended at journal acceptance; until then the record may be restricted. digital elevation model; formal verification; terrain analysis; hydrology; reproducible benchmark; Dafny; Lean 4; spatial computation guo ying gang PUBLIC https://creativecommons.org/licenses/by-nc-sa/4.0/ dataset Science Data Bank