Concern about potential spam from bot accounts linked to this project

[alephpiece]

Hey maintainers of leanprover-community!

I’ve noticed today that there are quite a few bot accounts leaving seemingly random and unhelpful comments on issues & PRs in various public repos. After digging around a bit, I came across this file in this project, which seems to be managed by your team. It looks like these bots might be connected to this.

I’m curious if this spam behavior is intentional or if something might have gone awry. These comments are unfortunately creating a bit of a mess for the maintainers of the affected repos. Could you shed some light on this? Any help or clarification would be greatly appreciated! Thanks!

Some affected issues:

• cherry-studio: [错误]: 对话输入框和文本编辑框前后台切换后的光标位置错误 CherryHQ/cherry-studio#5832
• ComfyUI: TypeError: LTXVImgToVideo.generate() got an unexpected keyword argument 'strength' comfyanonymous/ComfyUI#8037
• aider: Uncaught AttributeError in models.py line 1010 Aider-AI/aider#3989
• aws-sam-cli: sam local invoke --invoke-image not using supplied image tag aws/aws-sam-cli#8014
• zed: Accent Menu (Press-and-Hold for Accents) not working in Terminal panel on macOS zed-industries/zed#30446
• pot-desktop: 希望在“历史记录”中增加token记录 pot-app/pot-desktop#1102
• MoviePilog: [Feature Request]: 在网站资源浏览页面增加电影库已有电影的标志 jxxghp/MoviePilot#4254
• git-town: set-parent (changing parent branch in general) overwrites the title incorrectly in bitbucket PR for corresponding proposal git-town/git-town#4900
• HealthGPT: Inquiry About Training Script DCDmllm/HealthGPT#24
• podman-compose: Tests should check multiple podman versions containers/podman-compose#1196
• hydrogen: Update or drop linux/debian/control hydrogen-music/hydrogen#2147
• nanobind: [BUG]: Python 3.13.3 circular import wjakob/nanobind#1040
• react-navigation: Navigation popToTop() does not work, or in other words how to get to Home page? react-navigation/react-navigation#12590
• spring-framework: Update outdated example that uses JettyHttpHandlerAdapter in the reference manual spring-projects/spring-framework#34875
• serenity: Error Message under MacOS M1 UTM (QEMU Emulation Mode) SerenityOS/serenity#25924

Some affected PRs:

• chromium: Mistake chromium/chromium#303
• immich: fix: construct chinese languages from subtags immich-app/immich#18197
• circuit: chore(deps): update dependency mkdocs-material to v9.6.13 slackhq/circuit#2085
• dolibarr: Update users.lang Replace "Dolibarr login" by "External user login" in the contact form. Dolibarr/dolibarr#34088
• doris: branch-2.1: [fix](memory) Fix PODArray::add_num_element apache/doris#50785
• mame: taitotz.cpp: batlgr2a is the Side by Side cabinet revision + other stuff mamedev/mame#13691
• KeyMapper: New Crowdin Translations keymapperorg/KeyMapper#1691
• website: Fix video embeds breaking when start time is configured flutter/website#12000
• ruby: ZJIT: Stop padding side exits ruby/ruby#13295
• graal: [GR-64829] Remove JDK21 specific code in compiler. oracle/graal#11167
• teleport: Add .pnpm-store to .gitignore gravitational/teleport#54701
• Specs: Administration /Create CODE_OF_CONDUCT.md CocoaPods/Specs#14612

[bryangingechen]

My understanding is that those JSON files are created / updated whenever a PR in https://github.com/leanprover-community/mathlib4 is updated (including receiving a comment), so it's just a reflection of the fact that we received spam on PR leanprover-community/mathlib4#24736 (comment)

[alephpiece]

My understanding is that those JSON files are created / updated whenever a PR in https://github.com/leanprover-community/mathlib4 is updated (including receiving a comment), so it's just a reflection of the fact that we received spam on PR leanprover-community/mathlib4#24736 (comment)

Hey, thanks so much for the clarification! I’m sorry for any misunderstanding on my part. Thanks again for your help!