AutoGL: A web-based theorem prover implementing a PSPACE proof-search algorithm for Gödel–Löb provability logic (GL). The algorithm was developed in the joint paper "Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents" (published at GandALF, 2026) with my master's student Omar Taher. The tool offers a toggle for enabling or disabling a computation log: with the log disabled, the algorithm runs in PSPACE—matching the known PSPACE-completeness of GL—while enabling the log allows users to inspect the entire "computation tree" built during proof-search at the cost of exceeding this space bound. The implementation was developed by Omar Taher as part of his master's thesis at TU Dresden.