Skip to content

feat(MultiTapeTM): loglogn_equals_no_space - #901

Open
barni120400 wants to merge 64 commits into
leanprover:mainfrom
barni120400:feat/tm-space-gap
Open

feat(MultiTapeTM): loglogn_equals_no_space#901
barni120400 wants to merge 64 commits into
leanprover:mainfrom
barni120400:feat/tm-space-gap

Conversation

@barni120400

Copy link
Copy Markdown
Contributor

Prove SPACE(o(log log n)) = SPACE(1) for languages over any finite alphabet. Input shortening from #900 shows that every halting multitape Turing machine with a subloglog space bound already uses constant space.

crei and others added 30 commits August 3, 2026 12:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants