# RESEARCH_LOG

**Search date:** 2026-08-17  
**Purpose:** 每篇正式稿開寫前重新檢索當前 theorem-proving、scientific-modeling、history/philosophy 與官方 open-problem sources。

## Paper-level literature routing

- **LSI-PSD-01:** automated theorem proving as proof-state search; HERMES; Stepwise; Goedel; Clay NS / P vs NP.
- **LSI-PSD-02:** TheoremGraph; semantic theorem search; agentic theorem proving; proof-state search.
- **LSI-PSD-03:** representation sensitivity and semantic-preserving rewrites; ASSESS; TheoremGraph; theorem semantic search.
- **LSI-PSD-04:** proof trajectories, neuro-symbolic proof search, research-agent surveys, internal NS observatory.
- **LSI-PSD-05:** fixed-window novelty and local saturation design; automated theorem proving benchmark/search literature; internal NS observatory.
- **LSI-PSD-06:** proof graphs, route dependencies, confluence instrumentation, internal NS observatory.
- **LSI-PSD-07:** Models in Science; Minimal Model Explanations; Productive Idealizations; Effective Field Theory.
- **LSI-PSD-08:** LISDD missing-physics discovery; discrepancy modeling; productive idealization; official NS / P vs NP status.
- **LSI-PSD-09:** missing-physics discovery, controlled model discrepancy, minimal models; experimental design for missing physics.
- **LSI-PSD-10:** Goedel incompleteness; representation sensitivity; official Clay NS / P vs NP problem status.
- **LSI-PSD-11:** Norton on Carnot; ACS Priestley and Lavoisier history; aether-to-relativity history; idealization/minimal/EFT philosophy.
- **LSI-PSD-12:** TheoremGraph; large-scale theorem semantic search; HERMES; minimal agents; theorem-proving surveys; internal NS observatory.

## Key current sources

1. Olejniczak et al., *What are the Right Symmetries for Formal Theorem Proving?*, arXiv:2605.22257 (2026).
2. Kurgan et al., *TheoremGraph: Bridging Formal and Informal Mathematics*, arXiv:2606.25363 (2026).
3. *From Solvers to Research: Large Language Model-Driven Mathematical Discovery*, arXiv:2607.07779 (2026).
4. *HERMES: Towards Efficient and Verifiable Mathematical Reasoning*, arXiv:2511.18760, revised 2026.
5. He et al., *Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification*, arXiv:2603.19715 (2026).
6. *A Minimal Agent for Automated Theorem Proving*, arXiv:2602.24273 (2026).
7. *Semantic Search over 9 Million Mathematical Theorems*, arXiv:2602.05216 (2026).
8. Wang, *Where Is My Physics Wrong?*, arXiv:2606.23215 (2026).
9. Weingarten, *Productive Idealizations for Scientific Understanding* (2026 preprint).
10. Batterman & Rice, *Minimal Model Explanations*, Philosophy of Science 81(3), 2014.
11. Stanford Encyclopedia of Philosophy, *Models in Science*.
12. Norton, *How Analogy Helped Create the New Science of Thermodynamics*, Synthese 200:269 (2022).
13. American Chemical Society, Priestley / Lavoisier historical landmark resources.
14. Clay Mathematics Institute, official Navier--Stokes and P vs NP pages, accessed 2026-08-17.

## Search interpretation rule

Current literature is used as context and comparison, not as authority for the new LSI-PSD terminology. Terms such as Logic-Space Integration, Productive Mis-specification Window, sampling tiers, and Proof-Space Non-Conclusion Principle are introduced here as working constructs and remain subject to empirical and formal revision.