Skip to content

Add ja_jp translation - #137

Draft
virusbb001 wants to merge 151 commits into
leanprover-community:mainfrom
virusbb001:add-ja_JP-translation
Draft

virusbb001 wants to merge 151 commits into
leanprover-community:mainfrom
virusbb001:add-ja_JP-translation

Conversation

@virusbb001

@virusbb001 virusbb001 commented Apr 28, 2026 •

Copy link
Copy Markdown

I created Japanese (ja_JP) translations, but I am not good at lean nor mathematics so I need supervising translators.

Once the remaining tasks are complete, I will switch to "Ready".

TODOs:

  • Add ja_JP translation to lean4game (I will create pull request later)
  • Ask someone to supervise the translation
  • Should I squash all commits? > no need to squash commits,

チュートリアルステージと加算ステージの翻訳を改善
…ation

ja_JP: improve implication translation
@joneugster

Copy link
Copy Markdown
Collaborator

(btw, no need to squash commits, the entire PR will be squashed into one commit when merging)

@virusbb001

virusbb001 commented Sep 19, 2026 •

Copy link
Copy Markdown
Author

To be honest, feedback from the Japanese LEAN community indicated that the translation quality was poor.
Fortunately, a community member recommended an introductory guide to LEAN that aligns with NNG4, so we are currently re-translating the material using that as a reference.
However, compounded by the fact that I have become busy, the re-translation is expected to take some time to complete.
Since leaving a pull request open and inactive for an extended period is not ideal, I am considering closing it for the time being.

@TentativeConvert

Copy link
Copy Markdown
Contributor

I think it's better if you leave it open, at least as a draft, so that other potential translators can more easily find this thread and see that you're working on this.

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.

3 participants