diff --git a/scripts/fix-comments.py b/scripts/fix-comments.py
deleted file mode 100755
index f5a3de4157093..0000000000000
--- a/scripts/fix-comments.py
+++ /dev/null
@@ -1,162 +0,0 @@
-#!/usr/bin/env python3
-
-import sys
-import os
-from pathlib import Path
-import subprocess
-import re
-
-if len(sys.argv) != 2 or not sys.argv[1].endswith('.lean'):
-    print("usage: fix-comments.py X.lean")
-    sys.exit(1)
-
-leanfile = sys.argv[1]
-
-is_clean = subprocess.run(
-    ['git', 'status', '--untracked-files=no', '--porcelain'],
-    capture_output=True,
-    check=True,
-    encoding='utf-8').stdout.rstrip()
-
-if is_clean != "":
-    print("Certain files tracked by git have uncommitted changes.\n")
-    os.system("git status --untracked-files=no")
-    print("\n")
-    s = input("Type y to continue. ")
-    if s != 'y':
-        sys.exit(1)
-
-root_dir = subprocess.run(
-    ['git', 'rev-parse', '--show-toplevel'],
-    capture_output=True,
-    check=True,
-    encoding='utf-8').stdout.rstrip()
-
-align_files = subprocess.run(
-    ['git', 'grep', '-l', '^#align'],
-    cwd=root_dir,
-    capture_output=True,
-    check=True,
-    encoding='utf-8')
-
-name_map = dict()
-for f in align_files.stdout.splitlines():
-    with open(os.path.join(root_dir, f), encoding="utf-8") as fh:
-        contents = fh.read()
-        for p in contents.split(sep='\n#align')[1:]:
-            n3, n4, *_ = p.split(maxsplit=2)
-            name_map[n3] = n4
-
-def replace_names(s):
-    # Terrible hack to treat `.` as a word character
-    # (to match qualified names)
-    s = s.replace('.', 'Ᾰ')
-    # re.DOTALL means that `.` can also match a newline.
-    # `\A` and `\Z` match only at the start/end of the string respectively.
-    w = re.findall(r'(?:\b|\A).+?(?:\b|\Z)', s, flags=re.DOTALL)
-    for i in range(len(w)):
-        w[i] = w[i].replace('Ᾰ', '.')
-        w[i] = name_map.get(w[i], w[i])
-    return ''.join(w)
-
-def process_backticked_names(s):
-    w = s.split(sep='`')
-    for i in range(len(w)):
-        if i % 2 == 1:
-            w[i] = replace_names(w[i])
-    return '`'.join(w)
-
-rewritten_contents = ''
-
-in_block_comment = False
-in_line_comment = False
-prev_char = None
-comment_so_far = None           # contains end marker but not begin marker
-
-def finish_comment():
-    global rewritten_contents
-    global in_block_comment
-    global in_line_comment
-    global comment_so_far
-    if comment_so_far is not None:
-        rewritten_contents += process_backticked_names(comment_so_far)
-        in_block_comment = False
-        in_line_comment = False
-        comment_so_far = None
-
-with open(leanfile, encoding="utf-8") as F:
-    while 1:
-        char = F.read(1)
-        if not char:
-            finish_comment()
-            break
-
-        if in_block_comment or in_line_comment:
-            comment_so_far = comment_so_far + char
-        else:
-            rewritten_contents += char
-
-        if in_block_comment and prev_char == '-' and char == '/':
-            finish_comment()
-
-        if in_line_comment and char == '\n':
-            finish_comment()
-
-        if comment_so_far is None and prev_char == '/' and char == '-':
-            in_block_comment = True
-            comment_so_far = ''
-
-        if comment_so_far is None and prev_char == '-' and char == '-':
-            in_line_comment = True
-            comment_so_far = ''
-
-        prev_char = char
-
-def mktree(path, sha, tree=True):
-    if path == Path('.'):
-        return sha
-    if tree:
-        inp = f"040000 tree {sha}\t{path.name}"
-    else:
-        inp = f"100644 blob {sha}\t{path.name}"
-    tree_sha = subprocess.run(
-        ['git', 'mktree'],
-        cwd=root_dir,
-        input=inp,
-        capture_output=True,
-        check=True,
-        encoding='utf8').stdout.rstrip()
-    return mktree(path.parent, tree_sha)
-
-path = Path(subprocess.run(
-    ['git', 'ls-files', '--full-name', leanfile],
-    capture_output=True,
-    check=True,
-    encoding='utf-8').stdout.rstrip())
-
-blob_sha = subprocess.run(
-    ['git', 'hash-object', '-w', '--stdin'],
-    input=rewritten_contents,
-    cwd=root_dir,
-    capture_output=True,
-    check=True,
-    encoding='utf-8').stdout.rstrip()
-
-tree_sha = mktree(path, blob_sha, tree=False)
-
-print(f"The script will now interactively suggest changes to {leanfile}.\n")
-s = input("Type y to continue. ")
-if s != 'y':
-    sys.exit(1)
-
-subprocess.run(['git', 'restore', '--patch', '--source=' + tree_sha, '--', leanfile], check=True)
-
-r = subprocess.run(['git', 'diff', '--quiet', leanfile])
-if r.returncode == 0:
-    pass
-elif r.returncode == 1:           # file was changed
-    print("\nPerhaps you would now like to run:")
-    print(f"git add {leanfile} && git commit -m 'auto: naming'")
-else:
-    # something went wrong
-    r.check_returncode()